Language.Futhark.TypeChecker.Unify

Implementation of unification and other core type system building blocks.

Documentation

data Constraint

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

Show Constraint

Defined in Language.Futhark.TypeChecker.Unify

Methods

showsPrec :: Int -> Constraint -> ShowS

show :: Constraint -> String

showList :: [Constraint] -> ShowS

Located Constraint

Defined in Language.Futhark.TypeChecker.Unify

Methods

locOf :: Constraint -> Loc

locOfList :: [Constraint] -> Loc

data Usage

A usage that caused a type constraint.

Instances

Show Usage

Defined in Language.Futhark.TypeChecker.Unify

Methods

showsPrec :: Int -> Usage -> ShowS

show :: Usage -> String

showList :: [Usage] -> ShowS

Pretty Usage

Defined in Language.Futhark.TypeChecker.Unify

Methods

ppr :: Usage -> Doc

pprPrec :: Int -> Usage -> Doc

pprList :: [Usage] -> Doc

Located Usage

Defined in Language.Futhark.TypeChecker.Unify

Methods

locOf :: Usage -> Loc

locOfList :: [Usage] -> Loc

mkUsage :: SrcLoc -> String -> Usage

Construct a Usage from a location and a description.

mkUsage' :: SrcLoc -> Usage

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

type Level = Int

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)

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

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

Minimal complete definition

getConstraints, putConstraints, newTypeVar, newDimVar, curLevel, matchError, unifyError

Methods

getConstraints :: m Constraints

putConstraints :: Constraints -> m ()

modifyConstraints :: (Constraints -> Constraints) -> m ()

newTypeVar :: Monoid als => SrcLoc -> String -> m (TypeBase dim als)

newDimVar :: SrcLoc -> Rigidity -> String -> m VName

curLevel :: m Level

matchError :: Located loc => loc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a

unifyError :: Located loc => loc -> Notes -> BreadCrumbs -> Doc -> m a

data Rigidity

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

Constructors

Rigid RigidSource

Nonrigid

Instances

Eq Rigidity

Defined in Language.Futhark.TypeChecker.Unify

Methods

(==) :: Rigidity -> Rigidity -> Bool

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

Ord Rigidity

Defined in Language.Futhark.TypeChecker.Unify

Methods

compare :: Rigidity -> Rigidity -> Ordering

(<) :: Rigidity -> Rigidity -> Bool

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

(>) :: Rigidity -> Rigidity -> Bool

(>=) :: Rigidity -> Rigidity -> Bool

max :: Rigidity -> Rigidity -> Rigidity

min :: Rigidity -> Rigidity -> Rigidity

Show Rigidity

Defined in Language.Futhark.TypeChecker.Unify

Methods

showsPrec :: Int -> Rigidity -> ShowS

show :: Rigidity -> String

showList :: [Rigidity] -> ShowS

data RigidSource

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

Instances

Eq RigidSource

Defined in Language.Futhark.TypeChecker.Unify

Methods

(==) :: RigidSource -> RigidSource -> Bool

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

Ord RigidSource

Defined in Language.Futhark.TypeChecker.Unify

Methods

compare :: RigidSource -> RigidSource -> Ordering

(<) :: RigidSource -> RigidSource -> Bool

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

(>) :: RigidSource -> RigidSource -> Bool

(>=) :: RigidSource -> RigidSource -> Bool

max :: RigidSource -> RigidSource -> RigidSource

min :: RigidSource -> RigidSource -> RigidSource

Show RigidSource

Defined in Language.Futhark.TypeChecker.Unify

Methods

showsPrec :: Int -> RigidSource -> ShowS

show :: RigidSource -> String

showList :: [RigidSource] -> ShowS

data BreadCrumbs

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

Pretty BreadCrumbs

Defined in Language.Futhark.TypeChecker.Unify

Methods

ppr :: BreadCrumbs -> Doc

pprPrec :: Int -> BreadCrumbs -> Doc

pprList :: [BreadCrumbs] -> Doc

noBreadCrumbs :: BreadCrumbs

An empty path.

hasNoBreadCrumbs :: BreadCrumbs -> Bool

Is the path empty?

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

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

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 ()

Assert that this type must be zero-order.

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

Assert that this type must be valid as an array element.

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

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 -> PatType -> m PatType

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

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

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 ()

Assert that this type must support equality.

normPatType :: MonadUnify m => PatType -> m PatType

Replace any top-level type variable with its substitution.

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

Replace all type variables with their substitution.

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

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

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

Unifies two types.

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

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

unifyMostCommon :: MonadUnify m => Usage -> PatType -> PatType -> m (PatType, [VName])

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)])

Replace dimension mismatches with AnyDim.

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

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