record.idr

module Language

import Data.So

%default total

-- typechecks after removing "mutual"
mutual
    record SomeRec where
        constructor MkSomeRec

        WhereCondition  : Bool

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

    zz : Bool
    zz = some (MkSomeRec True)
    
{-
Errors (3)
/home/nickolay/workspace/Idris/horn/src/Test2.idr:14:10
When checking type of Language.some:
When checking an application of type constructor Data.So.So:
        No such variable WhereCondition

/home/nickolay/workspace/Idris/horn/src/Test2.idr:15:5
No type declaration for Language.some

/home/nickolay/workspace/Idris/horn/src/Test2.idr:18:10
When checking right hand side of zz with expected type
        Bool

No such variable some


-}