Safe Haskell	Safe-Inferred
Language	Haskell2010

Unison.Typechecker.Context

Synopsis

synthesizeClosed :: (BuiltinAnnotation loc, Var v, Ord loc, Show loc, Semigroup loc) => PrettyPrintEnv -> PatternMatchCoverageCheckAndKindInferenceSwitch -> Map Reference [Variance] -> [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)]
- | Warning (Warn v loc)
- | VarBinding v loc (Type v loc)
- | VarMention v loc
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, NESet 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 (CtxSegment v loc)
data Warn v loc = AbilityConcreteSubset [Type v loc] [Type v loc] (Term v loc) (Context 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 loc (Type v loc)
- | Marker v
data PathElement v loc
- = InSynthesize (Term v loc)
- | InSubtype (Type v loc) (Type v loc)
- | InSubAbilities [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
- | InActionRestriction
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, Measured (Info v loc) c) => c -> 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
- | RightNameWrongType
- | WrongNameRightType
- | SimilarNameRightType
- | SimilarNameWrongType
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 => Map Reference [Variance] -> 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, Semigroup loc) => PrettyPrintEnv -> PatternMatchCoverageCheckAndKindInferenceSwitch -> Map Reference [Variance] -> [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)]
Warning (Warn v loc)
VarBinding v loc (Type v loc)
VarMention v loc	The usage of a particular variable. We report the variable and its location so we can match a given source location with a specific symbol later in the LSP.

Instances

Instances details

(Var v, Show loc, Ord loc) => 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, NESet 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 (CtxSegment v loc)

Instances

Instances details

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

data Warn v loc Source #

Constructors

AbilityConcreteSubset [Type v loc] [Type v loc] (Term v loc) (Context v loc)

Instances

Instances details

(Var v, Ord loc) => Show (Warn v loc) Source #
Instance details Defined in Unison.Typechecker.Context Methods showsPrec :: Int -> Warn v loc -> ShowS # show :: Warn v loc -> String # showList :: [Warn 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. A context is a sequence of Elements (here represented as a finger tree), but not every sequence represents a valid context. A context is only valid if every type that occurs in the context is well scoped with regard to the previous variable bindings in the context.

We will refer to invalid trees as 'context segments' since they can be prefixed to become part of a valid context. Keeping track of the same context information for _every_ segment is important to avoiding some performance problems with a more naive implementation.

Constructors

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

Instances

Instances details

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

data PathElement v loc Source #

Constructors

InSynthesize (Term v loc)
InSubtype (Type v loc) (Type v loc)
InSubAbilities [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
InActionRestriction

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, Measured (Info v loc) c) => c -> 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
RightNameWrongType
WrongNameRightType
SimilarNameRightType
SimilarNameWrongType

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 => Map Reference [Variance] -> Type v loc -> Type v loc Source #

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