name.idr

module Language

import Data.So

%default total

record SomeRec where
    constructor MkSomeRec

    WhereCondition  : Bool

some : (rec : SomeRec) -> {auto so : So (Language.WhereCondition rec)} -> Bool
some rec = ?some_rhs

zz : Bool
zz = some (MkSomeRec True)

{-

Errors (1)
/home/nickolay/workspace/Idris/horn/src/Test2.idr:12:6
When checking type of Language.some:
When checking an application of type constructor Data.So.So:
        No such variable Language.WhereCondition


-}