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, Semigroup 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, Semigroup 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, Semigroup 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 [Either Name (NamedReference v loc)]
- freeNameToFuzzyTermsByShortName :: Map Name (Map Name [Either Name (NamedReference v loc)])
- topLevelComponents :: 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, Semigroup 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, Semigroup 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, Semigroup 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 [Either Name (NamedReference v loc)]
TDNR environment - maps short names like + to fully-qualified lists of named references whose full name matches the short name Example: + maps to [Nat.+, Float.+, Int.+]
This mapping is populated before typechecking with as few entries as are needed to help resolve variables needing TDNR in the file.
- Left means a term in the file (for which we don't have a type before typechecking)
- Right means a term/constructor in the namespace, or a constructor in the file (for which we do have a type before typechecking)
freeNameToFuzzyTermsByShortName :: Map Name (Map Name [Either Name (NamedReference v loc)])
This mapping is populated before typechecking with the top N fuzzy matches to provide suggestions to the user for each free name that could not be resolved with an exact match.
For each free name, a separate mapping with the same type as termsByShortname is provided.
topLevelComponents :: 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-3G24XkyMShKBxXCUvG3T87" '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 [Either Name (NamedReference v loc)])) :: (S1 ('MetaSel ('Just "freeNameToFuzzyTermsByShortName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name (Map Name [Either Name (NamedReference v loc)]))) :: S1 ('MetaSel ('Just "topLevelComponents") '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