Safe Haskell	Safe-Inferred
Language	Haskell2010

Unison.Typechecker

Description

This module is the primary interface to the Unison typechecker module Unison.Typechecker (admissibleTypeAt, check, check', checkAdmissible', equals, locals, subtype, isSubtype, synthesize, synthesize', typeAt, wellTyped) where

Synopsis

synthesize :: (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> PatternMatchCoverageCheckAndKindInferenceSwitch -> Env v loc -> Term v loc -> ResultT (Notes v loc) f (Type v loc)
synthesizeAndResolve :: (Monad f, Var v, Monoid loc, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> Env v loc -> TDNR f v loc (Type v loc)
check :: (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> Env v loc -> Term v loc -> Type v loc -> ResultT (Notes v loc) f (Type v loc)
wellTyped :: (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> Env v loc -> Term v loc -> f Bool
isEqual :: Var v => Type v loc -> Type v loc -> Bool
isSubtype :: Var v => Type v loc -> Type v loc -> Bool
fitsScheme :: Var v => Type v loc -> Type v loc -> Bool
data Env v loc = Env {
- ambientAbilities :: [Type v loc]
- typeLookup :: TypeLookup v loc
- termsByShortname :: Map Name [NamedReference v loc]
}
data Notes v loc = Notes {
- bugs :: Seq (CompilerBug v loc)
- errors :: Seq (ErrorNote v loc)
- infos :: Seq (InfoNote v loc)
}
data Resolution v loc = Resolution {
- resolvedName :: Text
- inferredType :: Type v loc
- resolvedLoc :: loc
- v :: v
- suggestions :: [Suggestion v loc]
}
type Name = Text
data NamedReference v loc = NamedReference {
- fqn :: Name
- fqnType :: Type v loc
- replacement :: Replacement v
}
data PatternMatchCoverageCheckAndKindInferenceSwitch
- = PatternMatchCoverageCheckAndKindInferenceSwitch'Enabled
- | PatternMatchCoverageCheckAndKindInferenceSwitch'Disabled

Documentation

synthesize :: (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> PatternMatchCoverageCheckAndKindInferenceSwitch -> Env v loc -> Term v loc -> ResultT (Notes v loc) f (Type v loc) Source #

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

synthesizeAndResolve :: (Monad f, Var v, Monoid loc, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> Env v loc -> TDNR f v loc (Type v loc) Source #

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

check :: (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> Env v loc -> Term v loc -> Type v loc -> ResultT (Notes v loc) f (Type v loc) Source #

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.

wellTyped :: (Monad f, Var v, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> Env v loc -> Term v loc -> f Bool Source #

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

isEqual :: Var v => Type v loc -> Type v loc -> Bool Source #

isSubtype :: Var v => Type v loc -> Type v loc -> Bool Source #

fitsScheme :: Var v => Type v loc -> Type v loc -> Bool Source #

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 fitsSchemeSymbol lhs rhs isTrue@ 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

data Env v loc Source #

Constructors

Env
Fields ambientAbilities :: [Type v loc] typeLookup :: TypeLookup v loc termsByShortname :: Map Name [NamedReference v loc]

Instances

Instances details

Generic (Env v loc) Source #
Instance details Defined in Unison.Typechecker Associated Types type Rep (Env v loc) :: Type -> Type # Methods from :: Env v loc -> Rep (Env v loc) x # to :: Rep (Env v loc) x -> Env v loc #
type Rep (Env v loc) Source #
Instance details Defined in Unison.Typechecker type Rep (Env v loc) = D1 ('MetaData "Env" "Unison.Typechecker" "unison-parser-typechecker-0.0.0-KNkVGbTXlis2lnVjsRIJUx" 'False) (C1 ('MetaCons "Env" 'PrefixI 'True) (S1 ('MetaSel ('Just "ambientAbilities") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type v loc]) :: (S1 ('MetaSel ('Just "typeLookup") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TypeLookup v loc)) :: S1 ('MetaSel ('Just "termsByShortname") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name [NamedReference v loc])))))

data Notes v loc Source #

Constructors

Notes
Fields bugs :: Seq (CompilerBug v loc) errors :: Seq (ErrorNote v loc) infos :: Seq (InfoNote v loc)

Instances

Instances details

Monoid (Notes v loc) Source #
Instance details Defined in Unison.Typechecker Methods mempty :: Notes v loc # mappend :: Notes v loc -> Notes v loc -> Notes v loc # mconcat :: [Notes v loc] -> Notes v loc #
Semigroup (Notes v loc) Source #
Instance details Defined in Unison.Typechecker Methods (<>) :: Notes v loc -> Notes v loc -> Notes v loc # sconcat :: NonEmpty (Notes v loc) -> Notes v loc # stimes :: Integral b => b -> Notes v loc -> Notes v loc #
(Var v, Show loc, Ord loc) => Show (Notes v loc) Source #
Instance details Defined in Unison.Typechecker Methods showsPrec :: Int -> Notes v loc -> ShowS # show :: Notes v loc -> String # showList :: [Notes v loc] -> ShowS #

data Resolution v loc Source #

Constructors

Resolution
Fields resolvedName :: Text inferredType :: Type v loc resolvedLoc :: loc v :: v suggestions :: [Suggestion v loc]

type Name = Text Source #

data NamedReference v loc Source #

Constructors

NamedReference
Fields fqn :: Name fqnType :: Type v loc replacement :: Replacement v

Instances

Instances details

Show v => Show (NamedReference v loc) Source #
Instance details Defined in Unison.Typechecker Methods showsPrec :: Int -> NamedReference v loc -> ShowS # show :: NamedReference v loc -> String # showList :: [NamedReference v loc] -> ShowS #

data PatternMatchCoverageCheckAndKindInferenceSwitch Source #

Constructors

PatternMatchCoverageCheckAndKindInferenceSwitch'Enabled
PatternMatchCoverageCheckAndKindInferenceSwitch'Disabled