futhark-0.20.0: An optimising compiler for a functional, array-oriented language.
Safe HaskellTrustworthy
LanguageHaskell2010

Language.Futhark.TypeChecker.Unify

Description

Implementation of unification and other core type system building blocks.

Synopsis

Documentation

data Constraint Source #

A constraint on a yet-ambiguous type variable.

Constructors

NoConstraint Liftedness Usage 
ParamType Liftedness SrcLoc 
Constraint StructType Usage 
Overloaded [PrimType] Usage 
HasFields (Map Name StructType) Usage 
Equality Usage 
HasConstrs (Map Name [StructType]) Usage 
ParamSize SrcLoc 
Size (Maybe (DimDecl VName)) Usage

Is not actually a type, but a term-level size, possibly already set to something specific.

UnknowableSize SrcLoc RigidSource

A size that does not unify with anything - created from the result of applying a function whose return size is existential, or otherwise hiding a size.

Instances

Instances details
Show Constraint Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Unify

Located Constraint Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Unify

data Usage Source #

A usage that caused a type constraint.

Instances

Instances details
Show Usage Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Unify

Methods

showsPrec :: Int -> Usage -> ShowS #

show :: Usage -> String #

showList :: [Usage] -> ShowS #

Pretty Usage Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Unify

Methods

ppr :: Usage -> Doc #

pprPrec :: Int -> Usage -> Doc #

pprList :: [Usage] -> Doc #

Located Usage Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Unify

Methods

locOf :: Usage -> Loc #

locOfList :: [Usage] -> Loc #

mkUsage :: SrcLoc -> String -> Usage Source #

Construct a Usage from a location and a description.

mkUsage' :: SrcLoc -> Usage Source #

Construct a Usage that has just a location, but no particular description.

type Level = Int Source #

The level at which a type variable is bound. Higher means deeper. We can only unify a type variable at level i with a type t if all type names that occur in t are at most at level i.

type Constraints = Map VName (Level, Constraint) Source #

Mapping from fresh type variables, instantiated from the type schemes of polymorphic functions, to (possibly) specific types as determined on application and the location of that application, or a partial constraint on their type.

class Monad m => MonadUnify m where Source #

Monads that which to perform unification must implement this type class.

data Rigidity Source #

The ridigity of a size variable. All rigid sizes are tagged with information about how they were generated.

Constructors

Rigid RigidSource 
Nonrigid 

data RigidSource Source #

The source of a rigid size.

Constructors

RigidArg (Maybe (QualName VName)) String

A function argument that is not a constant or variable name.

RigidRet (Maybe (QualName VName))

An existential return size.

RigidLoop 
RigidSlice (Maybe (DimDecl VName)) String

Produced by a complicated slice expression.

RigidRange

Produced by a complicated range expression.

RigidBound String

Produced by a range expression with this bound.

RigidCond StructType StructType

Mismatch in branches.

RigidUnify

Invented during unification.

RigidOutOfScope SrcLoc VName 

data BreadCrumbs Source #

Unification failures can occur deep down inside complicated types (consider nested records). We leave breadcrumbs behind us so we can report the path we took to find the mismatch.

Instances

Instances details
Pretty BreadCrumbs Source # 
Instance details

Defined in Language.Futhark.TypeChecker.Unify

hasNoBreadCrumbs :: BreadCrumbs -> Bool Source #

Is the path empty?

dimNotes :: (Located a, MonadUnify m) => a -> DimDecl VName -> m Notes Source #

Retrieve notes describing the purpose or origin of the given DimDecl. The location is used as the *current* location, for the purpose of reporting relative locations.

mkTypeVarName :: String -> Int -> Name Source #

Construct the name of a new type variable given a base description and a tag number (note that this is distinct from actually constructing a VName; the tag here is intended for human consumption but the machine does not care).

zeroOrderType :: (MonadUnify m, Pretty (ShapeDecl dim), Monoid as) => Usage -> String -> TypeBase dim as -> m () Source #

Assert that this type must be zero-order.

mustHaveConstr :: MonadUnify m => Usage -> Name -> StructType -> [StructType] -> m () Source #

In mustHaveConstr usage c t fs, the type t must have a constructor named c that takes arguments of types ts.

mustHaveField :: MonadUnify m => Usage -> Name -> PatternType -> m PatternType Source #

Assert that some type must have a field with this name and type.

mustBeOneOf :: MonadUnify m => [PrimType] -> Usage -> StructType -> m () Source #

Assert that this type must be one of the given primitive types.

equalityType :: (MonadUnify m, Pretty (ShapeDecl dim), Monoid as) => Usage -> TypeBase dim as -> m () Source #

Assert that this type must support equality.

normType :: MonadUnify m => StructType -> m StructType Source #

Replace any top-level type variable with its substitution.

normPatternType :: MonadUnify m => PatternType -> m PatternType Source #

Replace any top-level type variable with its substitution.

normTypeFully :: (Substitutable a, MonadUnify m) => a -> m a Source #

Replace all type variables with their substitution.

instantiateEmptyArrayDims :: MonadUnify m => SrcLoc -> String -> Rigidity -> TypeBase (DimDecl VName) als -> m (TypeBase (DimDecl VName) als, [VName]) Source #

Replace AnyDim dimensions that occur as PosImmediate or PosParam with a fresh NamedDim.

unify :: MonadUnify m => Usage -> StructType -> StructType -> m () Source #

Unifies two types.

expect :: MonadUnify m => Usage -> StructType -> StructType -> m () Source #

expect super sub checks that sub is a subtype of super.

unifyMostCommon :: MonadUnify m => Usage -> PatternType -> PatternType -> m (PatternType, [VName]) Source #

Like unification, but creates new size variables where mismatches occur. Returns the new dimensions thus created.

anyDimOnMismatch :: Monoid as => TypeBase (DimDecl VName) as -> TypeBase (DimDecl VName) as -> (TypeBase (DimDecl VName) as, [(DimDecl VName, DimDecl VName)]) Source #

Replace dimension mismatches with AnyDim.

doUnification :: SrcLoc -> [TypeParam] -> StructType -> StructType -> Either TypeError StructType Source #

Perform a unification of two types outside a monadic context. The type parameters are allowed to be instantiated; all other types are considered rigid.