Safe Haskell | None |
---|---|
Language | Haskell98 |
- splitProblem :: Maybe QName -> Problem -> TCM (Either SplitError SplitProblem)
- checkParsIfUnambiguous :: [QName] -> QName -> Args -> TCM ()
- wellFormedIndices :: Type -> TCM ()
- withTypesFrom :: Args -> Type -> TCM [(Arg Term, Dom Type)]
Documentation
:: Maybe QName | The definition we are checking at the moment. |
-> Problem | The current state of the lhs patterns. |
-> TCM (Either SplitError SplitProblem) |
Split a problem at the first constructor pattern which is actually of datatype type.
Or, if there is no constructor pattern left and the rest type is a record type and the first rest pattern is a projection pattern, split the rest type.
Implicit patterns should have been inserted.
checkParsIfUnambiguous :: [QName] -> QName -> Args -> TCM () Source
checkParsIfUnambiguous [c] d pars
checks that the data/record type
behind c
is has initial parameters (coming e.g. from a module instantiation)
that coincide with an prefix of pars
.
wellFormedIndices :: Type -> TCM () Source
Takes a type, which must be a data or record type application, and checks that the indices are constructors (or literals) applied to distinct variables which do not occur free in the parameters. For the purposes of this check parameters count as constructor arguments; parameters are reconstructed from the given type.
Precondition: The type must be a data or record type application.