Inferno.Infer

Documentation

type Constraint = Either (InfernoType, InfernoType, [TypeError SourcePos]) (Location SourcePos, TypeClass)

data TypeError a

Constructors

UnificationFail (Set TypeClass) InfernoType InfernoType (Location a)

ExpectedFunction (Set TypeClass) InfernoType InfernoType (Location a)

InfiniteType TV InfernoType (Location a)

UnboundNameInNamespace (Scoped ModuleName) (Either VCObjectHash Namespace) (Location a)

UnboundExtIdent (Scoped ModuleName) ExtIdent (Location a)

ImplicitVarTypeOverlap (Set TypeClass) ExtIdent InfernoType InfernoType (Location a)

UnificationMismatch (Set.Set TypeClass) InfernoType InfernoType (Location a) | Ambiguous [Constraint]

VarMultipleOccurrence Ident (Location a) (Location a)

IfConditionMustBeBool (Set TypeClass) InfernoType (Location a)

AssertConditionMustBeBool (Set TypeClass) InfernoType (Location a)

IfBranchesMustBeEqType (Set TypeClass) InfernoType InfernoType (Location a) (Location a)

CaseBranchesMustBeEqType (Set TypeClass) InfernoType InfernoType (Location a) (Location a)

PatternUnificationFail InfernoType InfernoType (Pat (Pinned VCObjectHash) a) (Location a)

PatternsMustBeEqType (Set TypeClass) InfernoType InfernoType (Pat (Pinned VCObjectHash) a) (Pat (Pinned VCObjectHash) a) (Location a) (Location a)

TypeClassNotFoundError (Set TypeClass) TypeClass (Location a)

TypeClassUnificationError InfernoType InfernoType TypeClass (Location a)

TypeClassNoPartialMatch TypeClass (Location a)

CouldNotFindTypeclassWitness (Set TypeClass) (Location a)

NonExhaustivePatternMatch Pattern (Location a)

UselessPattern (Maybe (Pat (Pinned VCObjectHash) a)) (Location a)

ModuleNameTaken ModuleName (Location a)

ModuleDoesNotExist ModuleName (Location a)

NameInModuleDoesNotExist ModuleName Ident (Location a)

AmbiguousName ModuleName Namespace (Location a)

Instances

Foldable TypeError

Defined in Inferno.Infer.Error

Methods

fold :: Monoid m => TypeError m -> m

foldMap :: Monoid m => (a -> m) -> TypeError a -> m

foldMap' :: Monoid m => (a -> m) -> TypeError a -> m

foldr :: (a -> b -> b) -> b -> TypeError a -> b

foldr' :: (a -> b -> b) -> b -> TypeError a -> b

foldl :: (b -> a -> b) -> b -> TypeError a -> b

foldl' :: (b -> a -> b) -> b -> TypeError a -> b

foldr1 :: (a -> a -> a) -> TypeError a -> a

foldl1 :: (a -> a -> a) -> TypeError a -> a

toList :: TypeError a -> [a]

null :: TypeError a -> Bool

length :: TypeError a -> Int

elem :: Eq a => a -> TypeError a -> Bool

maximum :: Ord a => TypeError a -> a

minimum :: Ord a => TypeError a -> a

sum :: Num a => TypeError a -> a

product :: Num a => TypeError a -> a

Substitutable Constraint

Defined in Inferno.Infer

Methods

apply :: Subst -> Constraint -> Constraint

ftv :: Constraint -> Set TV

Show a => Show (TypeError a)

Defined in Inferno.Infer.Error

Methods

showsPrec :: Int -> TypeError a -> ShowS

show :: TypeError a -> String

showList :: [TypeError a] -> ShowS

Eq a => Eq (TypeError a)

Defined in Inferno.Infer.Error

Methods

(==) :: TypeError a -> TypeError a -> Bool

(/=) :: TypeError a -> TypeError a -> Bool

Ord a => Ord (TypeError a)

Defined in Inferno.Infer.Error

Methods

compare :: TypeError a -> TypeError a -> Ordering

(<) :: TypeError a -> TypeError a -> Bool

(<=) :: TypeError a -> TypeError a -> Bool

(>) :: TypeError a -> TypeError a -> Bool

(>=) :: TypeError a -> TypeError a -> Bool

max :: TypeError a -> TypeError a -> TypeError a

min :: TypeError a -> TypeError a -> TypeError a

Substitutable (TypeError a)

Defined in Inferno.Infer.Error

Methods

apply :: Subst -> TypeError a -> TypeError a

ftv :: TypeError a -> Set TV

Corecursive (TypeError a)

Defined in Inferno.Infer.Error

Methods

embed :: Base (TypeError a) (TypeError a) -> TypeError a

ana :: (a0 -> Base (TypeError a) a0) -> a0 -> TypeError a

apo :: (a0 -> Base (TypeError a) (Either (TypeError a) a0)) -> a0 -> TypeError a

postpro :: Recursive (TypeError a) => (forall b. Base (TypeError a) b -> Base (TypeError a) b) -> (a0 -> Base (TypeError a) a0) -> a0 -> TypeError a

gpostpro :: (Recursive (TypeError a), Monad m) => (forall b. m (Base (TypeError a) b) -> Base (TypeError a) (m b)) -> (forall c. Base (TypeError a) c -> Base (TypeError a) c) -> (a0 -> Base (TypeError a) (m a0)) -> a0 -> TypeError a

Recursive (TypeError a)

Defined in Inferno.Infer.Error

Methods

project :: TypeError a -> Base (TypeError a) (TypeError a)

cata :: (Base (TypeError a) a0 -> a0) -> TypeError a -> a0

para :: (Base (TypeError a) (TypeError a, a0) -> a0) -> TypeError a -> a0

gpara :: (Corecursive (TypeError a), Comonad w) => (forall b. Base (TypeError a) (w b) -> w (Base (TypeError a) b)) -> (Base (TypeError a) (EnvT (TypeError a) w a0) -> a0) -> TypeError a -> a0

prepro :: Corecursive (TypeError a) => (forall b. Base (TypeError a) b -> Base (TypeError a) b) -> (Base (TypeError a) a0 -> a0) -> TypeError a -> a0

gprepro :: (Corecursive (TypeError a), Comonad w) => (forall b. Base (TypeError a) (w b) -> w (Base (TypeError a) b)) -> (forall c. Base (TypeError a) c -> Base (TypeError a) c) -> (Base (TypeError a) (w a0) -> a0) -> TypeError a -> a0

type Base (TypeError a)

Defined in Inferno.Infer.Error

type Base (TypeError a)

newtype Subst

Constructors

Subst (Map TV InfernoType)

Instances

Monoid Subst

Defined in Inferno.Types.Type

Methods

mempty :: Subst

mappend :: Subst -> Subst -> Subst

mconcat :: [Subst] -> Subst

Semigroup Subst

Defined in Inferno.Types.Type

Methods

(<>) :: Subst -> Subst -> Subst

sconcat :: NonEmpty Subst -> Subst

stimes :: Integral b => b -> Subst -> Subst

Show Subst

Defined in Inferno.Types.Type

Methods

showsPrec :: Int -> Subst -> ShowS

show :: Subst -> String

showList :: [Subst] -> ShowS

Eq Subst

Defined in Inferno.Types.Type

Methods

(==) :: Subst -> Subst -> Bool

(/=) :: Subst -> Subst -> Bool

Ord Subst

Defined in Inferno.Types.Type

Methods

compare :: Subst -> Subst -> Ordering

(<) :: Subst -> Subst -> Bool

(<=) :: Subst -> Subst -> Bool

(>) :: Subst -> Subst -> Bool

(>=) :: Subst -> Subst -> Bool

max :: Subst -> Subst -> Subst

min :: Subst -> Subst -> Subst

inferExpr :: Map ModuleName (PinnedModule m) -> Expr (Pinned VCObjectHash) SourcePos -> Either [TypeError SourcePos] (Expr (Pinned VCObjectHash) SourcePos, TCScheme, Map (Location SourcePos) (TypeMetadata TCScheme))

Solve for the top level type of an expression in a given environment

closeOver :: Set TypeClass -> ImplType -> TCScheme

Canonicalize and return the polymorphic toplevel type.

closeOverType :: InfernoType -> TCScheme

findTypeClassWitnesses :: Set TypeClass -> Maybe Int -> Set TypeClass -> Set TV -> [Subst]

This function encodes our typeclasses into CNF clauses for the SAT-solver. The translation works in the following way: Given a set of type-classes, e.g. `{requires addition on 'a int producing 'b ,requires addition on 'b 'b producing double}` we first compute all the matching instances from allClasses, in this case, we get: `requires addition on 'a int producing b matches: - `requires addition on int int producing int` - `requires addition on double int producing double` `requires addition on 'b 'b producing double` matches: - `requires addition on double double producing double` Now we translate each possible class instantiation into the following clauses: `requires addition on int int producing int` becomes: `'a_int - add_class_1_inst_1_arg_1` `'b_int - add_class_1_inst_1_arg_3` `add_class_1_inst_1_arg_1 / add_class_1_inst_1_arg_3 - add_class_1_inst_1` `requires addition on double int producing double` becomes: `'a_double - add_class_1_inst_2_arg_1` `'b_doube - add_class_1_inst_2_arg_3` `add_class_1_inst_2_arg_1 / add_class_1_inst_2_arg_3 - add_class_1_inst_2` We have to make sure that exactly one instance matches, i.e. `requires addition on int int producing int` or `requires addition on double int producing double`, but not both: `add_class_1_inst_1 XOR add_class_1_inst_2` Next we encode the second set of matching instances, namely `requires addition on double double producing double`: `'b_doube - add_class_2_inst_1_arg_1` `'b_doube - add_class_2_inst_1_arg_2` `add_class_2_inst_1_arg_1 / add_class_2_inst_1_arg_2 - add_class_2_inst_1` Since the second typeclass only matches one instance, we simply add it in as true: add_class_2_inst_1 Finally, we collect all the variables with all their possible types and encode the condition that exactly one type for each is matched: `'a_int XOR a_double `'b_int XOR b_double If the SAT solver returns SAT, we simply check which one of `'a_?` and `'b_?` is set to true in the resulting model. If the solver returns the model `'a_double b_double and we want to check for any more solutions, we simply add `-('a_double 'b_double)` (-a_double / -b_double in CNF) as a clause and re-run the solver. Once all assignments have been exhausted, we will get UNSAT.

inferTypeReps :: Set TypeClass -> TCScheme -> [InfernoType] -> InfernoType -> Either [TypeError SourcePos] [InfernoType]

Given a type signature and some concrete assignment of types (assumes inputTys and outputTy have no free variables) | this function computes the runtime reps

inferPossibleTypes :: Set TypeClass -> TCScheme -> [Maybe InfernoType] -> Maybe InfernoType -> Either [TypeError SourcePos] ([[InfernoType]], [InfernoType])

Orphan instances

Substitutable Constraint

Methods

apply :: Subst -> Constraint -> Constraint

ftv :: Constraint -> Set TV