| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Rzk.TypeCheck.Unify
Description
Unification, which in rzk is really subtyping: an extension type's faces, a shape's tope and the variance of the position all take part.
Synopsis
- inScope2 :: forall (n :: S) a. Distinct n => Binder -> TModality -> TermT n -> ScopedTermT n -> ScopedTermT n -> (forall (l :: S). (DExt n l, Distinct l) => NameBinder n l -> TermT l -> TermT l -> TypeCheck l a) -> TypeCheck n a
- alphaEq :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n Bool
- bySubtyping :: forall (n :: S). (TermT n -> TermT n -> TypeCheck n ()) -> TermT n -> TermT n -> TypeCheck n ()
- domainEntails :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
- unifyTopes :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
- unify :: forall (n :: S). Distinct n => Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
- unifyViaDecompose :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
- unifyTypes :: forall (n :: S). Distinct n => TermT n -> TermT n -> TermT n -> TypeCheck n ()
- unifyTerms :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n ()
- checkCoherence :: forall (n :: S). Distinct n => (TermT n, TermT n) -> (TermT n, TermT n) -> TypeCheck n ()
- unifyInCurrentContext :: forall (n :: S). Distinct n => Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n ()
Documentation
inScope2 :: forall (n :: S) a. Distinct n => Binder -> TModality -> TermT n -> ScopedTermT n -> ScopedTermT n -> (forall (l :: S). (DExt n l, Distinct l) => NameBinder n l -> TermT l -> TermT l -> TypeCheck l a) -> TypeCheck n a Source #
Open two scoped terms under one binder, so that the two sides of a comparison are compared as functions of the same variable.
alphaEq :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n Bool Source #
α-equivalence in the ambient scope.
bySubtyping :: forall (n :: S). (TermT n -> TermT n -> TypeCheck n ()) -> TermT n -> TermT n -> TypeCheck n () Source #
Run check super sub on the pair (expected, actual), oriented by the
ambient variance. Under Covariant the expected type is the supertype and
under Contravariant the actual one is. Invariant is normally handled
upstream by running both directions; we run both here as well, for safety.
domainEntails :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n () Source #
The domain of a shape-indexed function is contravariant, so the subtype's domain tope has to hold wherever the supertype's does. Shared by Π-types and by the lambdas that inhabit them.
unify :: forall (n :: S). Distinct n => Maybe (TermT n) -> TermT n -> TermT n -> TypeCheck n () Source #
unifyViaDecompose :: forall (n :: S). Distinct n => TermT n -> TermT n -> TypeCheck n () Source #
The syntactic fast path.
α-equivalence, not the structural equality the old representation used: two terms that differ only in a binder's name are the same term, and saying so here saves the whole unification below.
unifyTypes :: forall (n :: S). Distinct n => TermT n -> TermT n -> TermT n -> TypeCheck n () Source #