Safe Haskell	Safe-Inferred
Language	Haskell2010

Unison.Typechecker.Context

Synopsis

synthesizeClosed :: (BuiltinAnnotation loc, Var v, Ord loc, Show loc) => PrettyPrintEnv -> PatternMatchCoverageCheckAndKindInferenceSwitch -> [Type v loc] -> TypeLookup v loc -> Term v loc -> Result v loc (Type v loc)
data ErrorNote v loc = ErrorNote {
- cause :: Cause v loc
- path :: Seq (PathElement v loc)
}
data CompilerBug v loc
- = UnknownDecl Unknown Reference (Map Reference (DataDeclaration v loc))
- | UnknownConstructor Unknown ConstructorReference (DataDeclaration v loc)
- | UndeclaredTermVariable v (Context v loc)
- | RetractFailure (Element v loc) (Context v loc)
- | EmptyLetRec (Term v loc)
- | PatternMatchFailure
- | EffectConstructorHadMultipleEffects (Type v loc)
- | FreeVarsInTypeAnnotation (Set (TypeVar v loc))
- | UnannotatedReference Reference
- | MalformedPattern (Pattern loc)
- | UnknownTermReference Reference
- | UnknownExistentialVariable v (Context v loc)
- | IllegalContextExtension (Context v loc) (Element v loc) String
- | OtherBug String
data InfoNote v loc
- = SolvedBlank (Recorded loc) v (Type v loc)
- | Decision v loc (Term v loc)
- | TopLevelComponent [(v, Type v loc, RedundantTypeAnnotation)]
data Cause v loc
- = TypeMismatch (Context v loc)
- | IllFormedType (Context v loc)
- | UnknownSymbol loc v
- | UnknownTerm loc v [Suggestion v loc] (Type v loc)
- | AbilityCheckFailure [Type v loc] [Type v loc] (Context v loc)
- | AbilityEqFailure [Type v loc] [Type v loc] (Context v loc)
- | EffectConstructorWrongArgCount ExpectedArgCount ActualArgCount ConstructorReference
- | MalformedEffectBind (Type v loc) (Type v loc) [Type v loc]
- | PatternArityMismatch loc (Type v loc) Int
- | DuplicateDefinitions (NonEmpty (v, [loc]))
- | UnguardedLetRecCycle [v] [(v, Term v loc)]
- | ConcatPatternWithoutConstantLength loc (Type v loc)
- | HandlerOfUnexpectedType loc (Type v loc)
- | DataEffectMismatch Unknown Reference (DataDeclaration v loc)
- | UncoveredPatterns loc (NonEmpty (Pattern ()))
- | RedundantPattern loc
- | KindInferenceFailure (KindError v loc)
- | InaccessiblePattern loc
newtype Context v loc = Context [(Element v loc, Info v loc)]
type ActualArgCount = Int
type ExpectedArgCount = Int
type ConstructorId = Word64
data Element v loc
- = Var (TypeVar v loc)
- | Solved (Blank loc) v (Monotype v loc)
- | Ann v (Type v loc)
- | Marker v
data PathElement v loc
- = InSynthesize (Term v loc)
- | InSubtype (Type v loc) (Type v loc)
- | InEquate (Type v loc) (Type v loc)
- | InCheck (Term v loc) (Type v loc)
- | InInstantiateL v (Type v loc)
- | InInstantiateR (Type v loc) v
- | InSynthesizeApp (Type v loc) (Term v loc) Int
- | InFunctionCall [v] (Term v loc) (Type v loc) [Term v loc]
- | InAndApp
- | InOrApp
- | InIfCond
- | InIfBody loc
- | InVectorApp loc
- | InMatch loc
- | InMatchGuard
- | InMatchBody
type Term v loc = Term' (TypeVar v loc) v loc
type Type v loc = Type (TypeVar v loc) loc
type TypeVar v loc = TypeVar (Blank loc) v
data Result v loc a
- = Success !(Seq (InfoNote v loc)) !a
- | TypeError !(NESeq (ErrorNote v loc)) !(Seq (InfoNote v loc))
- | CompilerBug !(CompilerBug v loc) !(Seq (ErrorNote v loc)) !(Seq (InfoNote v loc))
data PatternMatchCoverageCheckAndKindInferenceSwitch
- = PatternMatchCoverageCheckAndKindInferenceSwitch'Enabled
- | PatternMatchCoverageCheckAndKindInferenceSwitch'Disabled
errorTerms :: ErrorNote v loc -> [Term v loc]
innermostErrorTerm :: ErrorNote v loc -> Maybe (Term v loc)
lookupAnn :: Ord v => Context v loc -> v -> Maybe (Type v loc)
lookupSolved :: Ord v => Context v loc -> v -> Maybe (Monotype v loc)
apply :: (Var v, Ord loc) => Context v loc -> Type v loc -> Type v loc
isEqual :: (Var v, Ord loc) => Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool
isSubtype :: (Var v, Ord loc) => Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool
fitsScheme :: (Var v, Ord loc) => Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool
isRedundant :: (Var v, Ord loc) => Type v loc -> Type v loc -> M v loc Bool
data Suggestion v loc = Suggestion {
- suggestionName :: Name
- suggestionType :: Type v loc
- suggestionReplacement :: Replacement v
- suggestionMatch :: SuggestionMatch
}
data Replacement v
- = ReplacementRef Referent
- | ReplacementVar v
data SuggestionMatch
- = Exact
- | WrongType
- | WrongName
isExact :: Suggestion v loc -> Bool
typeErrors :: Result v loc a -> Seq (ErrorNote v loc)
infoNotes :: Result v loc a -> Seq (InfoNote v loc)
data Unknown
- = Data
- | Effect
relax :: Var v => Ord loc => Type v loc -> Type v loc
generalizeAndUnTypeVar :: Var v => Type v a -> Type v a

Documentation

synthesizeClosed :: (BuiltinAnnotation loc, Var v, Ord loc, Show loc) => PrettyPrintEnv -> PatternMatchCoverageCheckAndKindInferenceSwitch -> [Type v loc] -> TypeLookup v loc -> Term v loc -> Result v loc (Type v loc) Source #

public interface to the typechecker

data ErrorNote v loc Source #

Constructors

ErrorNote
Fields cause :: Cause v loc path :: Seq (PathElement v loc)

Instances

Instances details

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

data CompilerBug v loc Source #

Constructors

UnknownDecl Unknown Reference (Map Reference (DataDeclaration v loc))
UnknownConstructor Unknown ConstructorReference (DataDeclaration v loc)
UndeclaredTermVariable v (Context v loc)
RetractFailure (Element v loc) (Context v loc)
EmptyLetRec (Term v loc)
PatternMatchFailure
EffectConstructorHadMultipleEffects (Type v loc)
FreeVarsInTypeAnnotation (Set (TypeVar v loc))
UnannotatedReference Reference
MalformedPattern (Pattern loc)
UnknownTermReference Reference
UnknownExistentialVariable v (Context v loc)
IllegalContextExtension (Context v loc) (Element v loc) String
OtherBug String

Instances

Instances details

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

data InfoNote v loc Source #

Constructors

SolvedBlank (Recorded loc) v (Type v loc)
Decision v loc (Term v loc)
TopLevelComponent [(v, Type v loc, RedundantTypeAnnotation)]

Instances

Instances details

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

data Cause v loc Source #

Constructors

TypeMismatch (Context v loc)
IllFormedType (Context v loc)
UnknownSymbol loc v
UnknownTerm loc v [Suggestion v loc] (Type v loc)
AbilityCheckFailure [Type v loc] [Type v loc] (Context v loc)
AbilityEqFailure [Type v loc] [Type v loc] (Context v loc)
EffectConstructorWrongArgCount ExpectedArgCount ActualArgCount ConstructorReference
MalformedEffectBind (Type v loc) (Type v loc) [Type v loc]
PatternArityMismatch loc (Type v loc) Int
DuplicateDefinitions (NonEmpty (v, [loc]))
UnguardedLetRecCycle [v] [(v, Term v loc)]
ConcatPatternWithoutConstantLength loc (Type v loc)
HandlerOfUnexpectedType loc (Type v loc)
DataEffectMismatch Unknown Reference (DataDeclaration v loc)
UncoveredPatterns loc (NonEmpty (Pattern ()))
RedundantPattern loc
KindInferenceFailure (KindError v loc)
InaccessiblePattern loc

Instances

Instances details

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

newtype Context v loc Source #

Constructors

Context [(Element v loc, Info v loc)]

Instances

Instances details

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

type ActualArgCount = Int Source #

type ExpectedArgCount = Int Source #

type ConstructorId = Word64 #

data Element v loc Source #

Elements of an ordered algorithmic context

Constructors

Var (TypeVar v loc)	A variable declaration
Solved (Blank loc) v (Monotype v loc)	`v` is solved to some monotype
Ann v (Type v loc)	`v` has type `a`, maybe quantified
Marker v	used for scoping

Instances

Instances details

Var v => Show (Element v loc) Source #
Instance details Defined in Unison.Typechecker.Context Methods showsPrec :: Int -> Element v loc -> ShowS # show :: Element v loc -> String # showList :: [Element v loc] -> ShowS #
(Ord loc, Var v) => Eq (Element v loc) Source #
Instance details Defined in Unison.Typechecker.Context Methods (==) :: Element v loc -> Element v loc -> Bool # (/=) :: Element v loc -> Element v loc -> Bool #

data PathElement v loc Source #

Constructors

InSynthesize (Term v loc)
InSubtype (Type v loc) (Type v loc)
InEquate (Type v loc) (Type v loc)
InCheck (Term v loc) (Type v loc)
InInstantiateL v (Type v loc)
InInstantiateR (Type v loc) v
InSynthesizeApp (Type v loc) (Term v loc) Int
InFunctionCall [v] (Term v loc) (Type v loc) [Term v loc]
InAndApp
InOrApp
InIfCond
InIfBody loc
InVectorApp loc
InMatch loc
InMatchGuard
InMatchBody

Instances

Instances details

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

type Term v loc = Term' (TypeVar v loc) v loc Source #

type Type v loc = Type (TypeVar v loc) loc Source #

type TypeVar v loc = TypeVar (Blank loc) v Source #

data Result v loc a Source #

Constructors

Success !(Seq (InfoNote v loc)) !a
TypeError !(NESeq (ErrorNote v loc)) !(Seq (InfoNote v loc))
CompilerBug !(CompilerBug v loc) !(Seq (ErrorNote v loc)) !(Seq (InfoNote v loc))

Instances

Instances details

MonadFix (Result v loc) Source #
Instance details Defined in Unison.Typechecker.Context Methods mfix :: (a -> Result v loc a) -> Result v loc a #
Applicative (Result v loc) Source #
Instance details Defined in Unison.Typechecker.Context Methods pure :: a -> Result v loc a # (<>) :: Result v loc (a -> b) -> Result v loc a -> Result v loc b # liftA2 :: (a -> b -> c) -> Result v loc a -> Result v loc b -> Result v loc c # (>) :: Result v loc a -> Result v loc b -> Result v loc b # (<*) :: Result v loc a -> Result v loc b -> Result v loc a #
Functor (Result v loc) Source #
Instance details Defined in Unison.Typechecker.Context Methods fmap :: (a -> b) -> Result v loc a -> Result v loc b # (<$) :: a -> Result v loc b -> Result v loc a #
Monad (Result v loc) Source #
Instance details Defined in Unison.Typechecker.Context Methods (>>=) :: Result v loc a -> (a -> Result v loc b) -> Result v loc b # (>>) :: Result v loc a -> Result v loc b -> Result v loc b # return :: a -> Result v loc a #

data PatternMatchCoverageCheckAndKindInferenceSwitch Source #

Constructors

PatternMatchCoverageCheckAndKindInferenceSwitch'Enabled
PatternMatchCoverageCheckAndKindInferenceSwitch'Disabled

errorTerms :: ErrorNote v loc -> [Term v loc] Source #

innermostErrorTerm :: ErrorNote v loc -> Maybe (Term v loc) Source #

lookupAnn :: Ord v => Context v loc -> v -> Maybe (Type v loc) Source #

lookupSolved :: Ord v => Context v loc -> v -> Maybe (Monotype v loc) Source #

apply :: (Var v, Ord loc) => Context v loc -> Type v loc -> Type v loc Source #

Replace any existentials with their solution in the context

isEqual :: (Var v, Ord loc) => Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool Source #

isSubtype :: (Var v, Ord loc) => Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool Source #

fitsScheme :: (Var v, Ord loc) => Type v loc -> Type v loc -> Either (CompilerBug v loc) Bool Source #

isRedundant :: (Var v, Ord loc) => Type v loc -> Type v loc -> M v loc Bool Source #

data Suggestion v loc Source #

Constructors

Suggestion
Fields suggestionName :: Name suggestionType :: Type v loc suggestionReplacement :: Replacement v suggestionMatch :: SuggestionMatch

Instances

Instances details

Show v => Show (Suggestion v loc) Source #
Instance details Defined in Unison.Typechecker.Context Methods showsPrec :: Int -> Suggestion v loc -> ShowS # show :: Suggestion v loc -> String # showList :: [Suggestion v loc] -> ShowS #
Var v => Eq (Suggestion v loc) Source #
Instance details Defined in Unison.Typechecker.Context Methods (==) :: Suggestion v loc -> Suggestion v loc -> Bool # (/=) :: Suggestion v loc -> Suggestion v loc -> Bool #

data Replacement v Source #

Constructors

ReplacementRef Referent
ReplacementVar v

Instances

Instances details

Show v => Show (Replacement v) Source #
Instance details Defined in Unison.Typechecker.Context Methods showsPrec :: Int -> Replacement v -> ShowS # show :: Replacement v -> String # showList :: [Replacement v] -> ShowS #
Eq v => Eq (Replacement v) Source #
Instance details Defined in Unison.Typechecker.Context Methods (==) :: Replacement v -> Replacement v -> Bool # (/=) :: Replacement v -> Replacement v -> Bool #
Ord v => Ord (Replacement v) Source #
Instance details Defined in Unison.Typechecker.Context Methods compare :: Replacement v -> Replacement v -> Ordering # (<) :: Replacement v -> Replacement v -> Bool # (<=) :: Replacement v -> Replacement v -> Bool # (>) :: Replacement v -> Replacement v -> Bool # (>=) :: Replacement v -> Replacement v -> Bool # max :: Replacement v -> Replacement v -> Replacement v # min :: Replacement v -> Replacement v -> Replacement v #

data SuggestionMatch Source #

Constructors

Exact
WrongType
WrongName

Instances

Instances details

Show SuggestionMatch Source #
Instance details Defined in Unison.Typechecker.Context Methods showsPrec :: Int -> SuggestionMatch -> ShowS # show :: SuggestionMatch -> String # showList :: [SuggestionMatch] -> ShowS #
Eq SuggestionMatch Source #
Instance details Defined in Unison.Typechecker.Context Methods (==) :: SuggestionMatch -> SuggestionMatch -> Bool # (/=) :: SuggestionMatch -> SuggestionMatch -> Bool #
Ord SuggestionMatch Source #
Instance details Defined in Unison.Typechecker.Context Methods compare :: SuggestionMatch -> SuggestionMatch -> Ordering # (<) :: SuggestionMatch -> SuggestionMatch -> Bool # (<=) :: SuggestionMatch -> SuggestionMatch -> Bool # (>) :: SuggestionMatch -> SuggestionMatch -> Bool # (>=) :: SuggestionMatch -> SuggestionMatch -> Bool # max :: SuggestionMatch -> SuggestionMatch -> SuggestionMatch # min :: SuggestionMatch -> SuggestionMatch -> SuggestionMatch #

isExact :: Suggestion v loc -> Bool Source #

typeErrors :: Result v loc a -> Seq (ErrorNote v loc) Source #

infoNotes :: Result v loc a -> Seq (InfoNote v loc) Source #

data Unknown Source #

Constructors

Data
Effect

Instances

Instances details

Show Unknown Source #
Instance details Defined in Unison.Typechecker.Context Methods showsPrec :: Int -> Unknown -> ShowS # show :: Unknown -> String # showList :: [Unknown] -> ShowS #

relax :: Var v => Ord loc => Type v loc -> Type v loc Source #

generalizeAndUnTypeVar :: Var v => Type v a -> Type v a Source #