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 StructRetType Usage

Overloaded [PrimType] Usage

HasFields Liftedness (Map Name StructType) Usage

Equality Usage

HasConstrs Liftedness (Map Name [StructType]) Usage

ParamSize SrcLoc

Size (Maybe Size) 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.

Constructors

Usage (Maybe Text) SrcLoc

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

pretty :: Usage -> Doc ann

prettyList :: [Usage] -> Doc ann

Located Usage

Defined in Language.Futhark.TypeChecker.Unify

Methods

locOf :: Usage -> Loc

locOfList :: [Usage] -> Loc

mkUsage :: SrcLoc -> Text -> 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 -> Name -> m (TypeBase dim als)

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

curLevel :: m Level

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

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

Instances

MonadUnify TermTypeM

Defined in Language.Futhark.TypeChecker.Terms.Monad

Methods

getConstraints :: TermTypeM Constraints

putConstraints :: Constraints -> TermTypeM ()

modifyConstraints :: (Constraints -> Constraints) -> TermTypeM ()

newTypeVar :: Monoid als => SrcLoc -> Name -> TermTypeM (TypeBase dim als)

newDimVar :: SrcLoc -> Rigidity -> Name -> TermTypeM VName

curLevel :: TermTypeM Level

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

unifyError :: Located loc => loc -> Notes -> BreadCrumbs -> Doc () -> TermTypeM 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

Show Rigidity

Defined in Language.Futhark.TypeChecker.Unify

Methods

showsPrec :: Int -> Rigidity -> ShowS

show :: Rigidity -> String

showList :: [Rigidity] -> ShowS

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

data RigidSource

The source of a rigid size.

Constructors

RigidArg (Maybe (QualName VName)) Text

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

RigidRet (Maybe (QualName VName))

An existential return size.

RigidLoop

RigidSlice (Maybe Size) Text

Produced by a complicated slice expression.

RigidRange

Produced by a complicated range expression.

RigidBound Text

Produced by a range expression with this bound.

RigidCond StructType StructType

Mismatch in branches.

RigidUnify

Invented during unification.

RigidOutOfScope SrcLoc VName

RigidCoerce

Blank dimension in coercion.

Instances

Show RigidSource

Defined in Language.Futhark.TypeChecker.Unify

Methods

showsPrec :: Int -> RigidSource -> ShowS

show :: RigidSource -> String

showList :: [RigidSource] -> ShowS

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

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

pretty :: BreadCrumbs -> Doc ann

prettyList :: [BreadCrumbs] -> Doc ann

noBreadCrumbs :: BreadCrumbs

An empty path.

hasNoBreadCrumbs :: BreadCrumbs -> Bool

Is the path empty?

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

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

zeroOrderType :: MonadUnify m => Usage -> Text -> StructType -> m ()

Assert that this type must be zero-order.

arrayElemType :: (MonadUnify m, Pretty (Shape dim), Monoid as) => Usage -> Text -> 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 (Shape 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 -> Rigidity -> RetTypeBase Size als -> m (TypeBase Size als, [VName])

Instantiate existential context in return type.

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.

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

Perform a unification of two types outside a monadic context. The first list of type parameters are rigid but may have liftedness constraints; the second list of type parameters are allowed to be instantiated. All other types are considered rigid with no constraints.