Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 [Either Name (NamedReference v loc)]
- topLevelComponents :: Map Name (NamedReference v loc)
- data Notes v loc = Notes {}
- 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
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
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 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
Env | |
|
Instances
Generic (Env v loc) Source # | |
type Rep (Env v loc) Source # | |
Defined in Unison.Typechecker type Rep (Env v loc) = D1 ('MetaData "Env" "Unison.Typechecker" "unison-parser-typechecker-0.0.0-JliU30UQmMa2dDW5SxUdL" '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 "topLevelComponents") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name (NamedReference v loc)))))) |
data Resolution v loc Source #
Resolution | |
|
data NamedReference v loc Source #
NamedReference | |
|
Instances
Show v => Show (NamedReference v loc) Source # | |
Defined in Unison.Typechecker showsPrec :: Int -> NamedReference v loc -> ShowS # show :: NamedReference v loc -> String # showList :: [NamedReference v loc] -> ShowS # |