Agda.TypeChecking.InstanceArguments

Documentation

findInstance :: MetaId -> Maybe [Candidate] -> TCM ()

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

shouldPostponeInstanceSearch :: (ReadTCState m, HasOptions m) => m Bool

postponeInstanceConstraints :: TCM a -> TCM a