test.idr

module Language

%default total

mutual
    data QuerySource : Type where
        Table           : (tableName : String) -> QuerySource
        SubQuery        : Bool -> QuerySource
        As              : (source : QuerySource) -> {auto prf : QuerySourceIsNotAliased source} -> (aliasName : String) -> QuerySource

    data QuerySourceIsNotAliased : QuerySource -> Type where
        BecauseItIsTable        : QuerySourceIsNotAliased (Table tableName)
        BecauseItIsSubquery     : QuerySourceIsNotAliased (SubQuery query)


some : QuerySource

some = Table "name" `As` "n"


{-

*Playground> :l Test2.i
/home/nickolay/workspace/Idris/horn/src/Test2.idr:18:1-28:
   |
18 | some = Table "name" `As` "n"
   | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Language.some is possibly not total due to: Language.BecauseItIsTable

*Test2>

-}