Safe Haskell | None |
---|---|

Language | Haskell98 |

- type Candidate = (Term, Type)
- type Candidates = [Candidate]
- initialIFSCandidates :: Type -> TCM (Maybe Candidates)
- initializeIFSMeta :: String -> Type -> TCM Term
- findInScope :: MetaId -> Maybe Candidates -> TCM ()
- findInScope' :: MetaId -> Candidates -> TCM (Maybe Candidates)
- rigidlyConstrainedMetas :: TCM [MetaId]
- checkCandidates :: MetaId -> Type -> Candidates -> TCM Candidates
- applyDroppingParameters :: Term -> Args -> TCM Term

# Documentation

type Candidate = (Term, Type) Source

A candidate solution for an instance meta is a term with its type.

type Candidates = [Candidate] Source

initialIFSCandidates :: Type -> TCM (Maybe Candidates) Source

Compute a list of instance candidates.
`Nothing`

if type is a meta, error if type is not eligible
for instance search.

initializeIFSMeta :: String -> Type -> TCM Term Source

`initializeIFSMeta s t`

generates an instance meta of type `t`

with suggested name `s`

.

findInScope :: MetaId -> Maybe Candidates -> TCM () Source

`findInScope m (v,a)s`

tries to instantiate on of the types `a`

s
of the candidate terms `v`

s 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.

findInScope' :: MetaId -> Candidates -> TCM (Maybe Candidates) Source

Result says whether we need to add constraint, and if so, the set of remaining candidates.

rigidlyConstrainedMetas :: TCM [MetaId] Source

A meta _M is rigidly constrained if there is a constraint _M us == D vs, for inert D. Such metas can safely be instantiated by recursive instance search, since the constraint limits the solution space.

checkCandidates :: MetaId -> Type -> Candidates -> TCM Candidates Source

Given a meta `m`

of type `t`

and a list of candidates `cands`

,
`checkCandidates m t cands`

returns a refined list of valid candidates.

applyDroppingParameters :: Term -> Args -> TCM Term Source

To preserve the invariant that a constructor is not applied to its
parameter arguments, we explicitly check whether function term
we are applying to arguments is a unapplied constructor.
In this case we drop the first `conPars`

arguments.
See Issue670a.
Andreas, 2013-11-07 Also do this for projections, see Issue670b.