Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
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
- flushInstanceConstraints :: TCM ()
- getInstanceCandidates :: MetaId -> TCM (Either Blocker [Candidate])
- getInstanceDefs :: TCM InstanceTable
- data OutputTypeName
  - = OutputTypeName QName
  - | OutputTypeVar
  - | OutputTypeVisiblePi
  - | OutputTypeNameNotYetKnown Blocker
  - | NoOutputTypeName
- getOutputTypeName :: Type -> TCM (Telescope, Term, OutputTypeName)
- addTypedInstance :: QName -> Type -> TCM ()
- readdTypedInstance :: QName -> Type -> TCM ()
- addTypedInstance' :: Bool -> Bool -> Maybe InstanceInfo -> QName -> Type -> TCM ()
- pruneTemporaryInstances :: Interface -> TCM Interface
- resolveInstanceHead :: QName -> TCM ()

# Documentation

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

`findInstance 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.

isInstanceConstraint :: Constraint -> Bool Source #

solveAwakeInstanceConstraints :: TCM () Source #

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

postponeInstanceConstraints :: TCM a -> TCM a Source #

flushInstanceConstraints :: TCM () Source #

getInstanceCandidates :: MetaId -> TCM (Either Blocker [Candidate]) Source #

Entry point for `tcGetInstances` primitive

getInstanceDefs :: TCM InstanceTable Source #

Try to solve the instance definitions whose type is not yet known, report an error if it doesn't work and return the instance table otherwise.

data OutputTypeName Source #

Constructors

OutputTypeName QName |
OutputTypeVar |
OutputTypeVisiblePi |
OutputTypeNameNotYetKnown Blocker |
NoOutputTypeName |

getOutputTypeName :: Type -> TCM (Telescope, Term, OutputTypeName) Source #

Strips all hidden and instance Pi's and return the argument telescope, the head term, and its name, if possible.

addTypedInstance Source #

Arguments

:: QName | Name of instance.
-> Type | Type of instance.
-> TCM () |

Register the definition with the given type as an instance. Issue warnings if instance is unusable.

readdTypedInstance Source #

Arguments

:: QName | Name of instance.
-> Type | Type of instance.
-> TCM () |

Like `addTypedInstance`, but delete any existing entries for the given name from the discrimination tree.

addTypedInstance' Source #

Arguments

:: Bool | Should we print warnings for unusable instance declarations?
-> Bool | Is this the second time we're adding this QName as an instance?
-> Maybe InstanceInfo | Is this instance a copy?
-> QName | Name of instance.
-> Type | Type of instance.
-> TCM () |

Register the definition with the given type as an instance.

pruneTemporaryInstances :: Interface -> TCM Interface Source #

Prune an `Interface` to remove any instances that would be inapplicable in child modules.

While in a section with visible arguments, we add any instances defined locally to the instance table: you have to be able to find them, after all! Conservatively, all of the local variables are turned into `FlexK`s, i.e., wildcards.

But when we leave such a section, these instances have no more value: even though they might technically be in scope, their types are malformed, since they have visible pis.

This function deletes these instances from the instance tree in the given signature to save on serialisation time *and* time spent checking for candidate validity in client modules. It can't do this directly in the TC state to prevent these instances from going out of scope before interaction (see #7196).

resolveInstanceHead :: QName -> TCM () Source #