Documentation

Infer the type of a Term, using a function to resolve the type of Ref constructors contained in that term.

Infer the type of a Term, using type-directed name resolution to attempt to resolve unknown symbols.

Check whether a term matches a type, using a function to resolve the type of Ref constructors contained in the term. Returns typ if successful, and a note about typechecking failure otherwise.

checkAdmissible e t` tests that `(f : t -> r) e` is well-typed. If t has quantifiers, these are moved outside, so if `t : forall a . a`, this will check that `(f : forall a . a -> a) e` is well typed. checkAdmissible' :: Var v => Term v -> Type v -> Either Note (Type v) checkAdmissible' term typ = synthesize' (Term.blank() ann_ tweak typ app_ term) where tweak (Type.ForallNamed' v body) = Type.forall() v (tweak body) tweak t = Type.arrow() t t | Returns True if the expression is well-typed, False otherwise

subtype a b is Right b iff f x is well-typed given x : a and f : b -> t. That is, if a value of type a can be passed to a function expecting a b, then `subtype a b` returns `Right b`. This function returns Left note with information about the reason for subtyping failure otherwise.

Example: subtype (forall a. a -> a) (Int -> Int) returns Right (Int -> Int). subtype :: Var v => Type v -> Type v -> Either Note (Type v) subtype t1 t2 = error "todo" let (t1', t2') = (ABT.vmap TypeVar.Universal t1, ABT.vmap TypeVar.Universal t2) in case Context.runM (Context.subtype t1' t2') (Context.MEnv Context.env0 [] Map.empty True) of Left e -> Left e Right _ -> Right t2

Returns true if subtype t1 t2 returns Right, false otherwise isSubtype :: Var v => Type v -> Type v -> Bool isSubtype t1 t2 = case subtype t1 t2 of Left _ -> False Right _ -> True

Returns true if the two type are equal, up to alpha equivalence and order of quantifier introduction. Note that alpha equivalence considers: `forall b a . a -> b -> a` and `forall a b . a -> b -> a` to be different types equals :: Var v => Type v -> Type v -> Bool equals t1 t2 = isSubtype t1 t2 && isSubtype t2 t1

Similar to isSubtype but treats t2 as a scheme where the outermost variables are existential rather than universal.

For example: let lhs = Unison.Type.ref () (Unison.Builtin.Decls.unitRef) rhs = Unison.Type.forall () (Unison.Var.named "x") (Unison.Type.var () (Unison.Var.named "x")) in fitsScheme Symbol lhs rhs is True@ although the lhs is not a subtype of the rhs.

fitsScheme is used to check that runnable types are a subtype of exists x. '{IO, Exception} x

Checks if the mismatch between two types is due to a missing delay, if so returns a tag for which type is missing the delay