| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.InstanceArguments
Synopsis
- findInstance :: MetaId -> Maybe [Candidate] -> TCM ()
- isInstanceConstraint :: Constraint -> Bool
- solveAwakeInstanceConstraints :: TCM ()
- shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool
- postponeInstanceConstraints :: TCM a -> TCM a
- getInstanceCandidates :: MetaId -> TCM (Either Blocker [Candidate])
Documentation
findInstance :: MetaId -> Maybe [Candidate] -> TCM () Source #
findInstance m (v,a)s tries to instantiate on of the types as
of the candidate terms vs to the type t of the metavariable m.
If successful, meta m is solved with the instantiation of v.
If unsuccessful, the constraint is regenerated, with possibly reduced
candidate set.
The list of candidates is equal to Nothing when the type of the meta
wasn't known when the constraint was generated. In that case, try to find
its type again.
isInstanceConstraint :: Constraint -> Bool Source #
shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool Source #
postponeInstanceConstraints :: TCM a -> TCM a Source #