-- | Type checker building blocks that do not involve unification.
module Language.Futhark.TypeChecker.Types
  ( checkTypeExp,
    renameRetType,
    subtypeOf,
    subuniqueOf,
    addAliasesFromType,
    checkForDuplicateNames,
    checkTypeParams,
    typeParamToArg,
    Subst (..),
    substFromAbbr,
    TypeSubs,
    Substitutable (..),
    substTypesAny,

    -- * Witnesses
    mustBeExplicitInType,
    mustBeExplicitInBinding,
    determineSizeWitnesses,
  )
where

import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State
import Data.Bifunctor
import Data.List (find, foldl', sort, unzip4, (\\))
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Futhark.Util (nubOrd)
import Futhark.Util.Pretty
import Language.Futhark
import Language.Futhark.Traversals
import Language.Futhark.TypeChecker.Monad

mustBeExplicitAux :: StructType -> M.Map VName Bool
mustBeExplicitAux :: StructType -> Map VName Bool
mustBeExplicitAux StructType
t =
  forall s a. State s a -> s -> s
execState (forall (f :: * -> *) fdim tdim als.
Applicative f =>
(Set VName -> DimPos -> fdim -> f tdim)
-> TypeBase fdim als -> f (TypeBase tdim als)
traverseDims forall {m :: * -> *}.
MonadState (Map VName Bool) m =>
Set VName -> DimPos -> Size -> m ()
onDim StructType
t) forall a. Monoid a => a
mempty
  where
    onDim :: Set VName -> DimPos -> Size -> m ()
onDim Set VName
bound DimPos
_ (NamedSize QualName VName
d)
      | forall vn. QualName vn -> vn
qualLeaf QualName VName
d forall a. Ord a => a -> Set a -> Bool
`S.member` Set VName
bound =
          forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \Map VName Bool
s -> forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Bool -> Bool -> Bool
(&&) (forall vn. QualName vn -> vn
qualLeaf QualName VName
d) Bool
False Map VName Bool
s
    onDim Set VName
_ DimPos
PosImmediate (NamedSize QualName VName
d) =
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \Map VName Bool
s -> forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Bool -> Bool -> Bool
(&&) (forall vn. QualName vn -> vn
qualLeaf QualName VName
d) Bool
False Map VName Bool
s
    onDim Set VName
_ DimPos
_ (NamedSize QualName VName
d) =
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Bool -> Bool -> Bool
(&&) (forall vn. QualName vn -> vn
qualLeaf QualName VName
d) Bool
True
    onDim Set VName
_ DimPos
_ Size
_ =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Determine which of the sizes in a type are used as sizes outside
-- of functions in the type, and which are not.  The former are said
-- to be "witnessed" by this type, while the latter are not.  In
-- practice, the latter means that the actual sizes must come from
-- somewhere else.
determineSizeWitnesses :: StructType -> (S.Set VName, S.Set VName)
determineSizeWitnesses :: StructType -> (Set VName, Set VName)
determineSizeWitnesses StructType
t =
  forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [k]
M.keys) (forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [k]
M.keys) forall a b. (a -> b) -> a -> b
$
    forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
M.partition Bool -> Bool
not forall a b. (a -> b) -> a -> b
$
      StructType -> Map VName Bool
mustBeExplicitAux StructType
t

-- | Figure out which of the sizes in a binding type must be passed
-- explicitly, because their first use is as something else than just
-- an array dimension.
mustBeExplicitInBinding :: StructType -> S.Set VName
mustBeExplicitInBinding :: StructType -> Set VName
mustBeExplicitInBinding StructType
bind_t =
  let ([StructType]
ts, StructType
ret) = forall dim as.
TypeBase dim as -> ([TypeBase dim ()], TypeBase dim ())
unfoldFunType StructType
bind_t
      alsoRet :: Map VName Bool -> Map VName Bool
alsoRet =
        forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith Bool -> Bool -> Bool
(&&) forall a b. (a -> b) -> a -> b
$
          forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$
            forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ forall as. TypeBase Size as -> Set VName
freeInType StructType
ret) forall a b. (a -> b) -> a -> b
$
              forall a. a -> [a]
repeat Bool
True
   in forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys forall a b. (a -> b) -> a -> b
$ forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ Map VName Bool -> Map VName Bool
alsoRet forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Map VName Bool -> StructType -> Map VName Bool
onType forall a. Monoid a => a
mempty [StructType]
ts
  where
    onType :: Map VName Bool -> StructType -> Map VName Bool
onType Map VName Bool
uses StructType
t = Map VName Bool
uses forall a. Semigroup a => a -> a -> a
<> StructType -> Map VName Bool
mustBeExplicitAux StructType
t -- Left-biased union.

-- | Figure out which of the sizes in a parameter type must be passed
-- explicitly, because their first use is as something else than just
-- an array dimension.
mustBeExplicitInType :: StructType -> S.Set VName
mustBeExplicitInType :: StructType -> Set VName
mustBeExplicitInType = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. StructType -> (Set VName, Set VName)
determineSizeWitnesses

-- | The two types are assumed to be structurally equal, but not
-- necessarily regarding sizes.  Adds aliases from the latter to the
-- former.
addAliasesFromType :: StructType -> PatType -> PatType
addAliasesFromType :: StructType -> PatType -> PatType
addAliasesFromType (Array ()
_ Uniqueness
u1 Shape Size
et1 ScalarTypeBase Size ()
shape1) (Array Set Alias
als Uniqueness
_ Shape Size
_ ScalarTypeBase Size ()
_) =
  forall dim as.
as
-> Uniqueness
-> Shape dim
-> ScalarTypeBase dim ()
-> TypeBase dim as
Array Set Alias
als Uniqueness
u1 Shape Size
et1 ScalarTypeBase Size ()
shape1
addAliasesFromType
  (Scalar (TypeVar ()
_ Uniqueness
u1 QualName VName
tv1 [TypeArg Size]
targs1))
  (Scalar (TypeVar Set Alias
als2 Uniqueness
_ QualName VName
_ [TypeArg Size]
_)) =
    forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar Set Alias
als2 Uniqueness
u1 QualName VName
tv1 [TypeArg Size]
targs1
addAliasesFromType (Scalar (Record Map Name StructType
ts1)) (Scalar (Record Map Name PatType
ts2))
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name StructType
ts1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name PatType
ts2,
    forall a. Ord a => [a] -> [a]
sort (forall k a. Map k a -> [k]
M.keys Map Name StructType
ts1) forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> [a]
sort (forall k a. Map k a -> [k]
M.keys Map Name PatType
ts2) =
      forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith StructType -> PatType -> PatType
addAliasesFromType Map Name StructType
ts1 Map Name PatType
ts2
addAliasesFromType
  (Scalar (Arrow ()
_ PName
mn1 StructType
pt1 (RetType [VName]
dims1 StructType
rt1)))
  (Scalar (Arrow Set Alias
as2 PName
_ StructType
_ (RetType [VName]
_ PatType
rt2))) =
    forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow Set Alias
as2 PName
mn1 StructType
pt1 (forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims1 PatType
rt1'))
    where
      rt1' :: PatType
rt1' = StructType -> PatType -> PatType
addAliasesFromType StructType
rt1 PatType
rt2
addAliasesFromType (Scalar (Sum Map Name [StructType]
cs1)) (Scalar (Sum Map Name [PatType]
cs2))
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name [StructType]
cs1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name [PatType]
cs2,
    forall a. Ord a => [a] -> [a]
sort (forall k a. Map k a -> [k]
M.keys Map Name [StructType]
cs1) forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> [a]
sort (forall k a. Map k a -> [k]
M.keys Map Name [PatType]
cs2) =
      forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum forall a b. (a -> b) -> a -> b
$ forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith StructType -> PatType -> PatType
addAliasesFromType) Map Name [StructType]
cs1 Map Name [PatType]
cs2
addAliasesFromType (Scalar (Prim PrimType
t)) PatType
_ = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim PrimType
t
addAliasesFromType StructType
t1 PatType
t2 =
  forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"addAliasesFromType invalid args: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (StructType
t1, PatType
t2)

-- | @unifyTypes uf t1 t2@ attempts to unify @t1@ and @t2@.  If
-- unification cannot happen, 'Nothing' is returned, otherwise a type
-- that combines the aliasing of @t1@ and @t2@ is returned.
-- Uniqueness is unified with @uf@.  Assumes sizes already match, and
-- always picks the size of the leftmost type.
unifyTypesU ::
  (Monoid als) =>
  (Uniqueness -> Uniqueness -> Maybe Uniqueness) ->
  TypeBase dim als ->
  TypeBase dim als ->
  Maybe (TypeBase dim als)
unifyTypesU :: forall als dim.
Monoid als =>
(Uniqueness -> Uniqueness -> Maybe Uniqueness)
-> TypeBase dim als -> TypeBase dim als -> Maybe (TypeBase dim als)
unifyTypesU Uniqueness -> Uniqueness -> Maybe Uniqueness
uf (Array als
als1 Uniqueness
u1 Shape dim
shape1 ScalarTypeBase dim ()
et1) (Array als
als2 Uniqueness
u2 Shape dim
_shape2 ScalarTypeBase dim ()
et2) =
  forall dim as.
as
-> Uniqueness
-> Shape dim
-> ScalarTypeBase dim ()
-> TypeBase dim as
Array (als
als1 forall a. Semigroup a => a -> a -> a
<> als
als2)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Uniqueness -> Uniqueness -> Maybe Uniqueness
uf Uniqueness
u1 Uniqueness
u2
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Shape dim
shape1
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall als dim.
Monoid als =>
(Uniqueness -> Uniqueness -> Maybe Uniqueness)
-> ScalarTypeBase dim als
-> ScalarTypeBase dim als
-> Maybe (ScalarTypeBase dim als)
unifyScalarTypes Uniqueness -> Uniqueness -> Maybe Uniqueness
uf ScalarTypeBase dim ()
et1 ScalarTypeBase dim ()
et2
unifyTypesU Uniqueness -> Uniqueness -> Maybe Uniqueness
uf (Scalar ScalarTypeBase dim als
t1) (Scalar ScalarTypeBase dim als
t2) = forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall als dim.
Monoid als =>
(Uniqueness -> Uniqueness -> Maybe Uniqueness)
-> ScalarTypeBase dim als
-> ScalarTypeBase dim als
-> Maybe (ScalarTypeBase dim als)
unifyScalarTypes Uniqueness -> Uniqueness -> Maybe Uniqueness
uf ScalarTypeBase dim als
t1 ScalarTypeBase dim als
t2
unifyTypesU Uniqueness -> Uniqueness -> Maybe Uniqueness
_ TypeBase dim als
_ TypeBase dim als
_ = forall a. Maybe a
Nothing

unifyScalarTypes ::
  (Monoid als) =>
  (Uniqueness -> Uniqueness -> Maybe Uniqueness) ->
  ScalarTypeBase dim als ->
  ScalarTypeBase dim als ->
  Maybe (ScalarTypeBase dim als)
unifyScalarTypes :: forall als dim.
Monoid als =>
(Uniqueness -> Uniqueness -> Maybe Uniqueness)
-> ScalarTypeBase dim als
-> ScalarTypeBase dim als
-> Maybe (ScalarTypeBase dim als)
unifyScalarTypes Uniqueness -> Uniqueness -> Maybe Uniqueness
_ (Prim PrimType
t1) (Prim PrimType
t2)
  | PrimType
t1 forall a. Eq a => a -> a -> Bool
== PrimType
t2 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim PrimType
t1
  | Bool
otherwise = forall a. Maybe a
Nothing
unifyScalarTypes Uniqueness -> Uniqueness -> Maybe Uniqueness
uf (TypeVar als
als1 Uniqueness
u1 QualName VName
tv1 [TypeArg dim]
targs1) (TypeVar als
als2 Uniqueness
u2 QualName VName
tv2 [TypeArg dim]
targs2)
  | QualName VName
tv1 forall a. Eq a => a -> a -> Bool
== QualName VName
tv2 = do
      Uniqueness
u3 <- Uniqueness -> Uniqueness -> Maybe Uniqueness
uf Uniqueness
u1 Uniqueness
u2
      [TypeArg dim]
targs3 <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM forall {dim}. TypeArg dim -> TypeArg dim -> Maybe (TypeArg dim)
unifyTypeArgs [TypeArg dim]
targs1 [TypeArg dim]
targs2
      forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar (als
als1 forall a. Semigroup a => a -> a -> a
<> als
als2) Uniqueness
u3 QualName VName
tv1 [TypeArg dim]
targs3
  | Bool
otherwise = forall a. Maybe a
Nothing
  where
    unifyTypeArgs :: TypeArg dim -> TypeArg dim -> Maybe (TypeArg dim)
unifyTypeArgs (TypeArgDim dim
d1 SrcLoc
loc) (TypeArgDim dim
_d2 SrcLoc
_) =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim dim
d1 SrcLoc
loc
    unifyTypeArgs (TypeArgType TypeBase dim ()
t1 SrcLoc
loc) (TypeArgType TypeBase dim ()
t2 SrcLoc
_) =
      forall dim. TypeBase dim () -> SrcLoc -> TypeArg dim
TypeArgType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall als dim.
Monoid als =>
(Uniqueness -> Uniqueness -> Maybe Uniqueness)
-> TypeBase dim als -> TypeBase dim als -> Maybe (TypeBase dim als)
unifyTypesU Uniqueness -> Uniqueness -> Maybe Uniqueness
uf TypeBase dim ()
t1 TypeBase dim ()
t2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
    unifyTypeArgs TypeArg dim
_ TypeArg dim
_ =
      forall a. Maybe a
Nothing
unifyScalarTypes Uniqueness -> Uniqueness -> Maybe Uniqueness
uf (Record Map Name (TypeBase dim als)
ts1) (Record Map Name (TypeBase dim als)
ts2)
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name (TypeBase dim als)
ts1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name (TypeBase dim als)
ts2,
    forall a. Ord a => [a] -> [a]
sort (forall k a. Map k a -> [k]
M.keys Map Name (TypeBase dim als)
ts1) forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> [a]
sort (forall k a. Map k a -> [k]
M.keys Map Name (TypeBase dim als)
ts2) =
      forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse
          (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall als dim.
Monoid als =>
(Uniqueness -> Uniqueness -> Maybe Uniqueness)
-> TypeBase dim als -> TypeBase dim als -> Maybe (TypeBase dim als)
unifyTypesU Uniqueness -> Uniqueness -> Maybe Uniqueness
uf))
          (forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name (TypeBase dim als)
ts1 Map Name (TypeBase dim als)
ts2)
unifyScalarTypes
  Uniqueness -> Uniqueness -> Maybe Uniqueness
uf
  (Arrow als
as1 PName
mn1 TypeBase dim ()
t1 (RetType [VName]
dims1 TypeBase dim als
t1'))
  (Arrow als
as2 PName
_ TypeBase dim ()
t2 (RetType [VName]
_ TypeBase dim als
t2')) =
    forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow (als
as1 forall a. Semigroup a => a -> a -> a
<> als
as2) PName
mn1
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall als dim.
Monoid als =>
(Uniqueness -> Uniqueness -> Maybe Uniqueness)
-> TypeBase dim als -> TypeBase dim als -> Maybe (TypeBase dim als)
unifyTypesU (forall a b c. (a -> b -> c) -> b -> a -> c
flip Uniqueness -> Uniqueness -> Maybe Uniqueness
uf) TypeBase dim ()
t1 TypeBase dim ()
t2
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall als dim.
Monoid als =>
(Uniqueness -> Uniqueness -> Maybe Uniqueness)
-> TypeBase dim als -> TypeBase dim als -> Maybe (TypeBase dim als)
unifyTypesU Uniqueness -> Uniqueness -> Maybe Uniqueness
uf TypeBase dim als
t1' TypeBase dim als
t2')
unifyScalarTypes Uniqueness -> Uniqueness -> Maybe Uniqueness
uf (Sum Map Name [TypeBase dim als]
cs1) (Sum Map Name [TypeBase dim als]
cs2)
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name [TypeBase dim als]
cs1 forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length Map Name [TypeBase dim als]
cs2,
    forall a. Ord a => [a] -> [a]
sort (forall k a. Map k a -> [k]
M.keys Map Name [TypeBase dim als]
cs1) forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> [a]
sort (forall k a. Map k a -> [k]
M.keys Map Name [TypeBase dim als]
cs2) =
      forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse
          (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (forall als dim.
Monoid als =>
(Uniqueness -> Uniqueness -> Maybe Uniqueness)
-> TypeBase dim als -> TypeBase dim als -> Maybe (TypeBase dim als)
unifyTypesU Uniqueness -> Uniqueness -> Maybe Uniqueness
uf)))
          (forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith (,) Map Name [TypeBase dim als]
cs1 Map Name [TypeBase dim als]
cs2)
unifyScalarTypes Uniqueness -> Uniqueness -> Maybe Uniqueness
_ ScalarTypeBase dim als
_ ScalarTypeBase dim als
_ = forall a. Maybe a
Nothing

-- | @x \`subtypeOf\` y@ is true if @x@ is a subtype of @y@ (or equal
-- to @y@), meaning @x@ is valid whenever @y@ is.  Ignores sizes.
-- Mostly used for checking uniqueness.
subtypeOf :: TypeBase () () -> TypeBase () () -> Bool
subtypeOf :: TypeBase () () -> TypeBase () () -> Bool
subtypeOf TypeBase () ()
t1 TypeBase () ()
t2 = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall als dim.
Monoid als =>
(Uniqueness -> Uniqueness -> Maybe Uniqueness)
-> TypeBase dim als -> TypeBase dim als -> Maybe (TypeBase dim als)
unifyTypesU Uniqueness -> Uniqueness -> Maybe Uniqueness
unifyUniqueness (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase () ()
t1) (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase () ()
t2)
  where
    unifyUniqueness :: Uniqueness -> Uniqueness -> Maybe Uniqueness
unifyUniqueness Uniqueness
u2 Uniqueness
u1 = if Uniqueness
u2 Uniqueness -> Uniqueness -> Bool
`subuniqueOf` Uniqueness
u1 then forall a. a -> Maybe a
Just Uniqueness
u1 else forall a. Maybe a
Nothing

-- | @x `subuniqueOf` y@ is true if @x@ is not less unique than @y@.
subuniqueOf :: Uniqueness -> Uniqueness -> Bool
subuniqueOf :: Uniqueness -> Uniqueness -> Bool
subuniqueOf Uniqueness
Nonunique Uniqueness
Unique = Bool
False
subuniqueOf Uniqueness
_ Uniqueness
_ = Bool
True

-- | Ensure that the dimensions of the RetType are unique by
-- generating new names for them.  This is to avoid name capture.
renameRetType :: MonadTypeChecker m => StructRetType -> m StructRetType
renameRetType :: forall (m :: * -> *).
MonadTypeChecker m =>
RetTypeBase Size () -> m (RetTypeBase Size ())
renameRetType (RetType [VName]
dims StructType
st)
  | [VName]
dims forall a. Eq a => a -> a -> Bool
/= forall a. Monoid a => a
mempty = do
      [VName]
dims' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). MonadTypeChecker m => VName -> m VName
newName [VName]
dims
      let m :: Map VName (Subst t)
m = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
dims forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t. Size -> Subst t
SizeSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Size
NamedSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. v -> QualName v
qualName) [VName]
dims'
          st' :: StructType
st' = forall a. Substitutable a => TypeSubs -> a -> a
applySubst (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` forall {t}. Map VName (Subst t)
m) StructType
st
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims' StructType
st'
  | Bool
otherwise =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims StructType
st

evalTypeExp ::
  MonadTypeChecker m =>
  TypeExp Name ->
  m (TypeExp VName, [VName], StructRetType, Liftedness)
evalTypeExp :: forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp (TEVar QualName Name
name SrcLoc
loc) = do
  (QualName VName
name', [TypeParam]
ps, RetTypeBase Size ()
t, Liftedness
l) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc
-> QualName Name
-> m (QualName VName, [TypeParam], RetTypeBase Size (), Liftedness)
lookupType SrcLoc
loc QualName Name
name
  RetTypeBase Size ()
t' <- forall (m :: * -> *).
MonadTypeChecker m =>
RetTypeBase Size () -> m (RetTypeBase Size ())
renameRetType RetTypeBase Size ()
t
  case [TypeParam]
ps of
    [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall vn. QualName vn -> SrcLoc -> TypeExp vn
TEVar QualName VName
name' SrcLoc
loc, [], RetTypeBase Size ()
t', Liftedness
l)
    [TypeParam]
_ ->
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type constructor"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall ann. [Doc ann] -> Doc ann
hsep (forall a ann. Pretty a => a -> Doc ann
pretty QualName Name
name forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [TypeParam]
ps))
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"used without any arguments."
--
evalTypeExp (TETuple [TypeExp Name]
ts SrcLoc
loc) = do
  ([TypeExp VName]
ts', [[VName]]
svars, [RetTypeBase Size ()]
ts_s, [Liftedness]
ls) <- forall a b c d. [(a, b, c, d)] -> ([a], [b], [c], [d])
unzip4 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp [TypeExp Name]
ts
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( forall vn. [TypeExp vn] -> SrcLoc -> TypeExp vn
TETuple [TypeExp VName]
ts' SrcLoc
loc,
      forall a. Monoid a => [a] -> a
mconcat [[VName]]
svars,
      forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall dim as. RetTypeBase dim as -> [VName]
retDims [RetTypeBase Size ()]
ts_s) forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. [TypeBase dim as] -> ScalarTypeBase dim as
tupleRecord forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall dim as. RetTypeBase dim as -> TypeBase dim as
retType [RetTypeBase Size ()]
ts_s,
      forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Ord a => a -> a -> a
max Liftedness
Unlifted [Liftedness]
ls
    )
--
evalTypeExp t :: TypeExp Name
t@(TERecord [(Name, TypeExp Name)]
fs SrcLoc
loc) = do
  -- Check for duplicate field names.
  let field_names :: [Name]
field_names = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, TypeExp Name)]
fs
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Ord a => [a] -> [a]
sort [Name]
field_names forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> [a]
sort (forall a. Ord a => [a] -> [a]
nubOrd [Name]
field_names)) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
      Doc ()
"Duplicate record fields in" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty TypeExp Name
t forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

  Map Name (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
checked <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, TypeExp Name)]
fs
  let fs' :: Map Name (TypeExp VName)
fs' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TypeExp VName
x, [VName]
_, RetTypeBase Size ()
_, Liftedness
_) -> TypeExp VName
x) Map Name (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
checked
      fs_svars :: [VName]
fs_svars = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(TypeExp VName
_, [VName]
y, RetTypeBase Size ()
_, Liftedness
_) -> [VName]
y) Map Name (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
checked
      ts_s :: Map Name (RetTypeBase Size ())
ts_s = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TypeExp VName
_, [VName]
_, RetTypeBase Size ()
z, Liftedness
_) -> RetTypeBase Size ()
z) Map Name (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
checked
      ls :: Map Name Liftedness
ls = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TypeExp VName
_, [VName]
_, RetTypeBase Size ()
_, Liftedness
v) -> Liftedness
v) Map Name (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
checked
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( forall vn. [(Name, TypeExp vn)] -> SrcLoc -> TypeExp vn
TERecord (forall k a. Map k a -> [(k, a)]
M.toList Map Name (TypeExp VName)
fs') SrcLoc
loc,
      [VName]
fs_svars,
      forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall dim as. RetTypeBase dim as -> [VName]
retDims Map Name (RetTypeBase Size ())
ts_s) forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
M.map forall dim as. RetTypeBase dim as -> TypeBase dim as
retType Map Name (RetTypeBase Size ())
ts_s,
      forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Ord a => a -> a -> a
max Liftedness
Unlifted Map Name Liftedness
ls
    )
--
evalTypeExp (TEArray SizeExp Name
d TypeExp Name
t SrcLoc
loc) = do
  ([VName]
d_svars, SizeExp VName
d', Size
d'') <- forall {m :: * -> *}.
MonadTypeChecker m =>
SizeExp Name -> m ([VName], SizeExp VName, Size)
checkSizeExp SizeExp Name
d
  (TypeExp VName
t', [VName]
svars, RetType [VName]
dims StructType
st, Liftedness
l) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp TypeExp Name
t
  case (Liftedness
l, forall as dim.
Monoid as =>
Uniqueness -> Shape dim -> TypeBase dim as -> TypeBase dim as
arrayOf Uniqueness
Nonunique (forall dim. [dim] -> Shape dim
Shape [Size
d'']) StructType
st) of
    (Liftedness
Unlifted, StructType
st') ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall vn. SizeExp vn -> TypeExp vn -> SrcLoc -> TypeExp vn
TEArray SizeExp VName
d' TypeExp VName
t' SrcLoc
loc,
          [VName]
svars,
          forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
d_svars forall a. [a] -> [a] -> [a]
++ [VName]
dims) StructType
st',
          Liftedness
Unlifted
        )
    (Liftedness
SizeLifted, StructType
_) ->
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        Doc ()
"Cannot create array with elements of size-lifted type"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty TypeExp Name
t)
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"(might cause irregular array)."
    (Liftedness
Lifted, StructType
_) ->
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        Doc ()
"Cannot create array with elements of lifted type"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty TypeExp Name
t)
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"(might contain function)."
  where
    checkSizeExp :: SizeExp Name -> m ([VName], SizeExp VName, Size)
checkSizeExp SizeExp Name
SizeExpAny = do
      VName
dv <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newTypeName Name
"d"
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ([VName
dv], forall vn. SizeExp vn
SizeExpAny, QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
dv)
    checkSizeExp (SizeExpConst Int
k SrcLoc
dloc) =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], forall vn. Int -> SrcLoc -> SizeExp vn
SizeExpConst Int
k SrcLoc
dloc, Int -> Size
ConstSize Int
k)
    checkSizeExp (SizeExpNamed QualName Name
v SrcLoc
dloc) = do
      QualName VName
v' <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName)
checkNamedSize SrcLoc
loc QualName Name
v
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], forall vn. QualName vn -> SrcLoc -> SizeExp vn
SizeExpNamed QualName VName
v' SrcLoc
dloc, QualName VName -> Size
NamedSize QualName VName
v')
--
evalTypeExp (TEUnique TypeExp Name
t SrcLoc
loc) = do
  (TypeExp VName
t', [VName]
svars, RetType [VName]
dims StructType
st, Liftedness
l) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp TypeExp Name
t
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall {dim} {as}. TypeBase dim as -> Bool
mayContainArray StructType
st) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) loc.
(MonadTypeChecker m, Located loc) =>
loc -> Doc () -> m ()
warn SrcLoc
loc forall a b. (a -> b) -> a -> b
$
      Doc ()
"Declaring" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty StructType
st) forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"as unique has no effect."
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall vn. TypeExp vn -> SrcLoc -> TypeExp vn
TEUnique TypeExp VName
t' SrcLoc
loc, [VName]
svars, forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims forall a b. (a -> b) -> a -> b
$ StructType
st forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
Unique, Liftedness
l)
  where
    mayContainArray :: TypeBase dim as -> Bool
mayContainArray (Scalar Prim {}) = Bool
False
    mayContainArray Array {} = Bool
True
    mayContainArray (Scalar (Record Map Name (TypeBase dim as)
fs)) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TypeBase dim as -> Bool
mayContainArray Map Name (TypeBase dim as)
fs
    mayContainArray (Scalar TypeVar {}) = Bool
True
    mayContainArray (Scalar Arrow {}) = Bool
False
    mayContainArray (Scalar (Sum Map Name [TypeBase dim as]
cs)) = (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any) TypeBase dim as -> Bool
mayContainArray Map Name [TypeBase dim as]
cs
--
evalTypeExp (TEArrow (Just Name
v) TypeExp Name
t1 TypeExp Name
t2 SrcLoc
loc) = do
  (TypeExp VName
t1', [VName]
svars1, RetType [VName]
dims1 StructType
st1, Liftedness
_) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp TypeExp Name
t1
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced [(Namespace
Term, Name
v)] forall a b. (a -> b) -> a -> b
$ do
    VName
v' <- forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term Name
v SrcLoc
loc
    forall (m :: * -> *) a.
MonadTypeChecker m =>
VName -> BoundV -> m a -> m a
bindVal VName
v' ([TypeParam] -> StructType -> BoundV
BoundV [] StructType
st1) forall a b. (a -> b) -> a -> b
$ do
      (TypeExp VName
t2', [VName]
svars2, RetType [VName]
dims2 StructType
st2, Liftedness
_) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp TypeExp Name
t2
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall vn.
Maybe vn -> TypeExp vn -> TypeExp vn -> SrcLoc -> TypeExp vn
TEArrow (forall a. a -> Maybe a
Just VName
v') TypeExp VName
t1' TypeExp VName
t2' SrcLoc
loc,
          [VName]
svars1 forall a. [a] -> [a] -> [a]
++ [VName]
dims1 forall a. [a] -> [a] -> [a]
++ [VName]
svars2,
          forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty (VName -> PName
Named VName
v') StructType
st1 (forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims2 StructType
st2),
          Liftedness
Lifted
        )
--
evalTypeExp (TEArrow Maybe Name
Nothing TypeExp Name
t1 TypeExp Name
t2 SrcLoc
loc) = do
  (TypeExp VName
t1', [VName]
svars1, RetType [VName]
dims1 StructType
st1, Liftedness
_) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp TypeExp Name
t1
  (TypeExp VName
t2', [VName]
svars2, RetType [VName]
dims2 StructType
st2, Liftedness
_) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp TypeExp Name
t2
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( forall vn.
Maybe vn -> TypeExp vn -> TypeExp vn -> SrcLoc -> TypeExp vn
TEArrow forall a. Maybe a
Nothing TypeExp VName
t1' TypeExp VName
t2' SrcLoc
loc,
      [VName]
svars1 forall a. [a] -> [a] -> [a]
++ [VName]
dims1 forall a. [a] -> [a] -> [a]
++ [VName]
svars2,
      forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow forall a. Monoid a => a
mempty PName
Unnamed StructType
st1 forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims2 StructType
st2,
      Liftedness
Lifted
    )
--
evalTypeExp (TEDim [Name]
dims TypeExp Name
t SrcLoc
loc) = do
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced (forall a b. (a -> b) -> [a] -> [b]
map (Namespace
Term,) [Name]
dims) forall a b. (a -> b) -> a -> b
$ do
    [VName]
dims' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
Term) SrcLoc
loc) [Name]
dims
    forall {m :: * -> *} {a}.
MonadTypeChecker m =>
[VName] -> m a -> m a
bindDims [VName]
dims' forall a b. (a -> b) -> a -> b
$ do
      (TypeExp VName
t', [VName]
svars, RetType [VName]
t_dims StructType
st, Liftedness
l) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp TypeExp Name
t
      let (Set VName
witnessed, Set VName
_) = StructType -> (Set VName, Set VName)
determineSizeWitnesses StructType
st
      case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (forall a. Ord a => a -> Set a -> Bool
`S.notMember` Set VName
witnessed) [VName]
dims' of
        Just VName
d ->
          forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. Doc ann -> Doc ann -> Doc ann
withIndexLink Doc ()
"unused-existential" forall a b. (a -> b) -> a -> b
$
            Doc ()
"Existential size "
              forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
d)
              forall a. Semigroup a => a -> a -> a
<> Doc ()
" not used as array size."
        Maybe VName
Nothing ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure
            ( forall vn. [vn] -> TypeExp vn -> SrcLoc -> TypeExp vn
TEDim [VName]
dims' TypeExp VName
t' SrcLoc
loc,
              [VName]
svars,
              forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
dims' forall a. [a] -> [a] -> [a]
++ [VName]
t_dims) StructType
st,
              forall a. Ord a => a -> a -> a
max Liftedness
l Liftedness
SizeLifted
            )
  where
    bindDims :: [VName] -> m a -> m a
bindDims [] m a
m = m a
m
    bindDims (VName
d : [VName]
ds) m a
m =
      forall (m :: * -> *) a.
MonadTypeChecker m =>
VName -> BoundV -> m a -> m a
bindVal VName
d ([TypeParam] -> StructType -> BoundV
BoundV [] forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim forall a b. (a -> b) -> a -> b
$ IntType -> PrimType
Signed IntType
Int64) forall a b. (a -> b) -> a -> b
$ [VName] -> m a -> m a
bindDims [VName]
ds m a
m
--
evalTypeExp t :: TypeExp Name
t@(TESum [(Name, [TypeExp Name])]
cs SrcLoc
loc) = do
  let constructors :: [Name]
constructors = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, [TypeExp Name])]
cs
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Ord a => [a] -> [a]
sort [Name]
constructors forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> [a]
sort (forall a. Ord a => [a] -> [a]
nubOrd [Name]
constructors)) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
      Doc ()
"Duplicate constructors in" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty TypeExp Name
t

  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
constructors forall a. Ord a => a -> a -> Bool
< Int
256) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty Doc ()
"Sum types must have less than 256 constructors."

  Map
  Name [(TypeExp VName, [VName], RetTypeBase Size (), Liftedness)]
checked <- (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, [TypeExp Name])]
cs
  let cs' :: Map Name [TypeExp VName]
cs' = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\(TypeExp VName
x, [VName]
_, RetTypeBase Size ()
_, Liftedness
_) -> TypeExp VName
x) Map
  Name [(TypeExp VName, [VName], RetTypeBase Size (), Liftedness)]
checked
      cs_svars :: [VName]
cs_svars = (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap) (\(TypeExp VName
_, [VName]
y, RetTypeBase Size ()
_, Liftedness
_) -> [VName]
y) Map
  Name [(TypeExp VName, [VName], RetTypeBase Size (), Liftedness)]
checked
      ts_s :: Map Name [RetTypeBase Size ()]
ts_s = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\(TypeExp VName
_, [VName]
_, RetTypeBase Size ()
z, Liftedness
_) -> RetTypeBase Size ()
z) Map
  Name [(TypeExp VName, [VName], RetTypeBase Size (), Liftedness)]
checked
      ls :: [Liftedness]
ls = (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (\(TypeExp VName
_, [VName]
_, RetTypeBase Size ()
_, Liftedness
v) -> Liftedness
v) Map
  Name [(TypeExp VName, [VName], RetTypeBase Size (), Liftedness)]
checked
  forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( forall vn. [(Name, [TypeExp vn])] -> SrcLoc -> TypeExp vn
TESum (forall k a. Map k a -> [(k, a)]
M.toList Map Name [TypeExp VName]
cs') SrcLoc
loc,
      [VName]
cs_svars,
      forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall dim as. RetTypeBase dim as -> [VName]
retDims) Map Name [RetTypeBase Size ()]
ts_s) forall a b. (a -> b) -> a -> b
$
        forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$
          forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum forall a b. (a -> b) -> a -> b
$
            forall a b k. (a -> b) -> Map k a -> Map k b
M.map (forall a b. (a -> b) -> [a] -> [b]
map forall dim as. RetTypeBase dim as -> TypeBase dim as
retType) Map Name [RetTypeBase Size ()]
ts_s,
      forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall a. Ord a => a -> a -> a
max Liftedness
Unlifted [Liftedness]
ls
    )
evalTypeExp ote :: TypeExp Name
ote@TEApply {} = do
  (QualName Name
tname, SrcLoc
tname_loc, [TypeArgExp Name]
targs) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name -> m (QualName Name, SrcLoc, [TypeArgExp Name])
rootAndArgs TypeExp Name
ote
  (QualName VName
tname', [TypeParam]
ps, RetTypeBase Size ()
tname_t, Liftedness
l) <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc
-> QualName Name
-> m (QualName VName, [TypeParam], RetTypeBase Size (), Liftedness)
lookupType SrcLoc
tloc QualName Name
tname
  RetType [VName]
t_dims StructType
t <- forall (m :: * -> *).
MonadTypeChecker m =>
RetTypeBase Size () -> m (RetTypeBase Size ())
renameRetType RetTypeBase Size ()
tname_t
  if forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArgExp Name]
targs
    then
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
tloc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type constructor"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty QualName Name
tname)
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"requires"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeParam]
ps)
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"arguments, but provided"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArgExp Name]
targs) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
    else do
      ([TypeArgExp VName]
targs', [[VName]]
dims, [Map VName (Subst (RetTypeBase Size ()))]
substs) <- forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM forall {m :: * -> *} {k}.
(MonadTypeChecker m, Eq k, IsName k) =>
TypeParamBase k
-> TypeArgExp Name
-> m (TypeArgExp VName, [VName],
      Map k (Subst (RetTypeBase Size ())))
checkArgApply [TypeParam]
ps [TypeArgExp Name]
targs
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\TypeExp VName
x TypeArgExp VName
y -> forall vn. TypeExp vn -> TypeArgExp vn -> SrcLoc -> TypeExp vn
TEApply TypeExp VName
x TypeArgExp VName
y SrcLoc
tloc) (forall vn. QualName vn -> SrcLoc -> TypeExp vn
TEVar QualName VName
tname' SrcLoc
tname_loc) [TypeArgExp VName]
targs',
          [],
          forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
t_dims forall a. [a] -> [a] -> [a]
++ forall a. Monoid a => [a] -> a
mconcat [[VName]]
dims) forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => TypeSubs -> a -> a
applySubst (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` forall a. Monoid a => [a] -> a
mconcat [Map VName (Subst (RetTypeBase Size ()))]
substs) StructType
t,
          Liftedness
l
        )
  where
    tloc :: SrcLoc
tloc = forall a. Located a => a -> SrcLoc
srclocOf TypeExp Name
ote

    rootAndArgs :: MonadTypeChecker m => TypeExp Name -> m (QualName Name, SrcLoc, [TypeArgExp Name])
    rootAndArgs :: forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name -> m (QualName Name, SrcLoc, [TypeArgExp Name])
rootAndArgs (TEVar QualName Name
qn SrcLoc
loc) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName Name
qn, SrcLoc
loc, [])
    rootAndArgs (TEApply TypeExp Name
op TypeArgExp Name
arg SrcLoc
_) = do
      (QualName Name
op', SrcLoc
loc, [TypeArgExp Name]
args) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name -> m (QualName Name, SrcLoc, [TypeArgExp Name])
rootAndArgs TypeExp Name
op
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (QualName Name
op', SrcLoc
loc, [TypeArgExp Name]
args forall a. [a] -> [a] -> [a]
++ [TypeArgExp Name
arg])
    rootAndArgs TypeExp Name
te' =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError (forall a. Located a => a -> SrcLoc
srclocOf TypeExp Name
te') forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty TypeExp Name
te') forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"is not a type constructor."

    checkArgApply :: TypeParamBase k
-> TypeArgExp Name
-> m (TypeArgExp VName, [VName],
      Map k (Subst (RetTypeBase Size ())))
checkArgApply (TypeParamDim k
pv SrcLoc
_) (TypeArgExpDim (SizeExpNamed QualName Name
v SrcLoc
dloc) SrcLoc
loc) = do
      QualName VName
v' <- forall (m :: * -> *).
MonadTypeChecker m =>
SrcLoc -> QualName Name -> m (QualName VName)
checkNamedSize SrcLoc
loc QualName Name
v
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall vn. SizeExp vn -> SrcLoc -> TypeArgExp vn
TypeArgExpDim (forall vn. QualName vn -> SrcLoc -> SizeExp vn
SizeExpNamed QualName VName
v' SrcLoc
dloc) SrcLoc
loc,
          [],
          forall k a. k -> a -> Map k a
M.singleton k
pv forall a b. (a -> b) -> a -> b
$ forall t. Size -> Subst t
SizeSubst forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize QualName VName
v'
        )
    checkArgApply (TypeParamDim k
pv SrcLoc
_) (TypeArgExpDim (SizeExpConst Int
x SrcLoc
dloc) SrcLoc
loc) =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall vn. SizeExp vn -> SrcLoc -> TypeArgExp vn
TypeArgExpDim (forall vn. Int -> SrcLoc -> SizeExp vn
SizeExpConst Int
x SrcLoc
dloc) SrcLoc
loc,
          [],
          forall k a. k -> a -> Map k a
M.singleton k
pv forall a b. (a -> b) -> a -> b
$ forall t. Size -> Subst t
SizeSubst forall a b. (a -> b) -> a -> b
$ Int -> Size
ConstSize Int
x
        )
    checkArgApply (TypeParamDim k
pv SrcLoc
_) (TypeArgExpDim SizeExp Name
SizeExpAny SrcLoc
loc) = do
      VName
d <- forall (m :: * -> *). MonadTypeChecker m => Name -> m VName
newTypeName Name
"d"
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall vn. SizeExp vn -> SrcLoc -> TypeArgExp vn
TypeArgExpDim forall vn. SizeExp vn
SizeExpAny SrcLoc
loc,
          [VName
d],
          forall k a. k -> a -> Map k a
M.singleton k
pv forall a b. (a -> b) -> a -> b
$ forall t. Size -> Subst t
SizeSubst forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
d
        )
    checkArgApply (TypeParamType Liftedness
_ k
pv SrcLoc
_) (TypeArgExpType TypeExp Name
te) = do
      (TypeExp VName
te', [VName]
svars, RetType [VName]
dims StructType
st, Liftedness
_) <- forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp TypeExp Name
te
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        ( forall vn. TypeExp vn -> TypeArgExp vn
TypeArgExpType TypeExp VName
te',
          [VName]
svars forall a. [a] -> [a] -> [a]
++ [VName]
dims,
          forall k a. k -> a -> Map k a
M.singleton k
pv forall a b. (a -> b) -> a -> b
$ forall t. [TypeParam] -> t -> Subst t
Subst [] forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] StructType
st
        )
    checkArgApply TypeParamBase k
p TypeArgExp Name
a =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
tloc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        Doc ()
"Type argument"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty TypeArgExp Name
a
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"not valid for a type parameter"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty TypeParamBase k
p forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

-- | Check a type expression, producing:
--
-- * The checked expression.
-- * Size variables for any anonymous sizes in the expression.
-- * The elaborated type.
-- * The liftedness of the type.
checkTypeExp ::
  MonadTypeChecker m =>
  TypeExp Name ->
  m (TypeExp VName, [VName], StructRetType, Liftedness)
checkTypeExp :: forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
checkTypeExp TypeExp Name
te = do
  forall (m :: * -> *). MonadTypeChecker m => TypeExp Name -> m ()
checkForDuplicateNamesInType TypeExp Name
te
  forall (m :: * -> *).
MonadTypeChecker m =>
TypeExp Name
-> m (TypeExp VName, [VName], RetTypeBase Size (), Liftedness)
evalTypeExp TypeExp Name
te

-- | Check for duplication of names inside a binding group.
checkForDuplicateNames ::
  MonadTypeChecker m => [UncheckedTypeParam] -> [UncheckedPat] -> m ()
checkForDuplicateNames :: forall (m :: * -> *).
MonadTypeChecker m =>
[UncheckedTypeParam] -> [UncheckedPat] -> m ()
checkForDuplicateNames [UncheckedTypeParam]
tps [UncheckedPat]
pats = (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
`evalStateT` forall a. Monoid a => a
mempty) forall a b. (a -> b) -> a -> b
$ do
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {b} {t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadState (Map (Namespace, b) SrcLoc) (t m), Pretty b,
 MonadTypeChecker m, MonadTrans t, Ord b) =>
TypeParamBase b -> t m ()
checkTypeParam [UncheckedTypeParam]
tps
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {b} {t :: (* -> *) -> * -> *} {m :: * -> *} {f :: * -> *}.
(MonadState (Map (Namespace, b) SrcLoc) (t m), Pretty b,
 MonadTypeChecker m, MonadTrans t, Ord b) =>
PatBase f b -> t m ()
checkPat [UncheckedPat]
pats
  where
    checkTypeParam :: TypeParamBase b -> t m ()
checkTypeParam (TypeParamType Liftedness
_ b
v SrcLoc
loc) = forall {a} {b} {a} {t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadState (Map (a, b) a) (t m), Located a, Pretty b,
 MonadTypeChecker m, MonadTrans t, Ord b, Ord a) =>
a -> b -> a -> t m ()
seen Namespace
Type b
v SrcLoc
loc
    checkTypeParam (TypeParamDim b
v SrcLoc
loc) = forall {a} {b} {a} {t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadState (Map (a, b) a) (t m), Located a, Pretty b,
 MonadTypeChecker m, MonadTrans t, Ord b, Ord a) =>
a -> b -> a -> t m ()
seen Namespace
Term b
v SrcLoc
loc

    checkPat :: PatBase f b -> t m ()
checkPat (Id b
v f PatType
_ SrcLoc
loc) = forall {a} {b} {a} {t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadState (Map (a, b) a) (t m), Located a, Pretty b,
 MonadTypeChecker m, MonadTrans t, Ord b, Ord a) =>
a -> b -> a -> t m ()
seen Namespace
Term b
v SrcLoc
loc
    checkPat (PatParens PatBase f b
p SrcLoc
_) = PatBase f b -> t m ()
checkPat PatBase f b
p
    checkPat (PatAttr AttrInfo b
_ PatBase f b
p SrcLoc
_) = PatBase f b -> t m ()
checkPat PatBase f b
p
    checkPat Wildcard {} = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    checkPat (TuplePat [PatBase f b]
ps SrcLoc
_) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ PatBase f b -> t m ()
checkPat [PatBase f b]
ps
    checkPat (RecordPat [(Name, PatBase f b)]
fs SrcLoc
_) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (PatBase f b -> t m ()
checkPat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Name, PatBase f b)]
fs
    checkPat (PatAscription PatBase f b
p TypeExp b
_ SrcLoc
_) = PatBase f b -> t m ()
checkPat PatBase f b
p
    checkPat PatLit {} = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    checkPat (PatConstr Name
_ f PatType
_ [PatBase f b]
ps SrcLoc
_) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ PatBase f b -> t m ()
checkPat [PatBase f b]
ps

    seen :: a -> b -> a -> t m ()
seen a
ns b
v a
loc = do
      Maybe a
already <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (a
ns, b
v)
      case Maybe a
already of
        Just a
prev_loc ->
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError a
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
              Doc ()
"Name"
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty b
v)
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"also bound at"
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Located a => a -> [Char]
locStr a
prev_loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
        Maybe a
Nothing ->
          forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (a
ns, b
v) a
loc

-- | Check whether the type contains arrow types that define the same
-- parameter.  These might also exist further down, but that's not
-- really a problem - we mostly do this checking to help the user,
-- since it is likely an error, but it's easy to assign a semantics to
-- it (normal name shadowing).
checkForDuplicateNamesInType ::
  MonadTypeChecker m =>
  TypeExp Name ->
  m ()
checkForDuplicateNamesInType :: forall (m :: * -> *). MonadTypeChecker m => TypeExp Name -> m ()
checkForDuplicateNamesInType = forall {a} {m :: * -> *}.
(MonadTypeChecker m, Pretty a, Ord a) =>
Map a SrcLoc -> TypeExp a -> m ()
check forall a. Monoid a => a
mempty
  where
    bad :: a -> loc -> a -> m a
bad a
v loc
loc a
prev_loc =
      forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError loc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
        Doc ()
"Name"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty a
v)
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"also bound at"
          forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Located a => a -> [Char]
locStr a
prev_loc) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."

    check :: Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen (TEArrow (Just a
v) TypeExp a
t1 TypeExp a
t2 SrcLoc
loc)
      | Just SrcLoc
prev_loc <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
v Map a SrcLoc
seen =
          forall {m :: * -> *} {a} {loc} {a} {a}.
(MonadTypeChecker m, Pretty a, Located loc, Located a) =>
a -> loc -> a -> m a
bad a
v SrcLoc
loc SrcLoc
prev_loc
      | Bool
otherwise =
          Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen' TypeExp a
t1 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen' TypeExp a
t2
      where
        seen' :: Map a SrcLoc
seen' = forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert a
v SrcLoc
loc Map a SrcLoc
seen
    check Map a SrcLoc
seen (TEArrow Maybe a
Nothing TypeExp a
t1 TypeExp a
t2 SrcLoc
_) =
      Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen TypeExp a
t1 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen TypeExp a
t2
    check Map a SrcLoc
seen (TETuple [TypeExp a]
ts SrcLoc
_) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen) [TypeExp a]
ts
    check Map a SrcLoc
seen (TERecord [(Name, TypeExp a)]
fs SrcLoc
_) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Name, TypeExp a)]
fs
    check Map a SrcLoc
seen (TEUnique TypeExp a
t SrcLoc
_) = Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen TypeExp a
t
    check Map a SrcLoc
seen (TESum [(Name, [TypeExp a])]
cs SrcLoc
_) = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Name, [TypeExp a])]
cs
    check Map a SrcLoc
seen (TEApply TypeExp a
t1 (TypeArgExpType TypeExp a
t2) SrcLoc
_) =
      Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen TypeExp a
t1 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen TypeExp a
t2
    check Map a SrcLoc
seen (TEApply TypeExp a
t1 TypeArgExpDim {} SrcLoc
_) =
      Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen TypeExp a
t1
    check Map a SrcLoc
seen (TEDim (a
v : [a]
vs) TypeExp a
t SrcLoc
loc)
      | Just SrcLoc
prev_loc <- forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup a
v Map a SrcLoc
seen =
          forall {m :: * -> *} {a} {loc} {a} {a}.
(MonadTypeChecker m, Pretty a, Located loc, Located a) =>
a -> loc -> a -> m a
bad a
v SrcLoc
loc SrcLoc
prev_loc
      | Bool
otherwise =
          Map a SrcLoc -> TypeExp a -> m ()
check (forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert a
v SrcLoc
loc Map a SrcLoc
seen) (forall vn. [vn] -> TypeExp vn -> SrcLoc -> TypeExp vn
TEDim [a]
vs TypeExp a
t SrcLoc
loc)
    check Map a SrcLoc
seen (TEDim [] TypeExp a
t SrcLoc
_) =
      Map a SrcLoc -> TypeExp a -> m ()
check Map a SrcLoc
seen TypeExp a
t
    check Map a SrcLoc
_ TEArray {} = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    check Map a SrcLoc
_ TEVar {} = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | @checkTypeParams ps m@ checks the type parameters @ps@, then
-- invokes the continuation @m@ with the checked parameters, while
-- extending the monadic name map with @ps@.
checkTypeParams ::
  MonadTypeChecker m =>
  [TypeParamBase Name] ->
  ([TypeParamBase VName] -> m a) ->
  m a
checkTypeParams :: forall (m :: * -> *) a.
MonadTypeChecker m =>
[UncheckedTypeParam] -> ([TypeParam] -> m a) -> m a
checkTypeParams [UncheckedTypeParam]
ps [TypeParam] -> m a
m =
  forall (m :: * -> *) a.
MonadTypeChecker m =>
[(Namespace, Name)] -> m a -> m a
bindSpaced (forall a b. (a -> b) -> [a] -> [b]
map forall {b}. TypeParamBase b -> (Namespace, b)
typeParamSpace [UncheckedTypeParam]
ps) forall a b. (a -> b) -> a -> b
$
    [TypeParam] -> m a
m forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadState (Map (Namespace, Name) SrcLoc) (t m),
 MonadTypeChecker m, MonadTrans t) =>
UncheckedTypeParam -> t m TypeParam
checkTypeParam [UncheckedTypeParam]
ps) forall a. Monoid a => a
mempty
  where
    typeParamSpace :: TypeParamBase b -> (Namespace, b)
typeParamSpace (TypeParamDim b
pv SrcLoc
_) = (Namespace
Term, b
pv)
    typeParamSpace (TypeParamType Liftedness
_ b
pv SrcLoc
_) = (Namespace
Type, b
pv)

    checkParamName :: Namespace -> Name -> SrcLoc -> t m VName
checkParamName Namespace
ns Name
v SrcLoc
loc = do
      Maybe SrcLoc
seen <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Namespace
ns, Name
v)
      case Maybe SrcLoc
seen of
        Just SrcLoc
prev ->
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
              Doc ()
"Type parameter"
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall a ann. Pretty a => a -> Doc ann
pretty Name
v)
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"previously defined at"
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (forall a. Located a => a -> [Char]
locStr SrcLoc
prev) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
        Maybe SrcLoc
Nothing -> do
          forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Namespace
ns, Name
v) SrcLoc
loc
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadTypeChecker m =>
Namespace -> Name -> SrcLoc -> m VName
checkName Namespace
ns Name
v SrcLoc
loc

    checkTypeParam :: UncheckedTypeParam -> t m TypeParam
checkTypeParam (TypeParamDim Name
pv SrcLoc
loc) =
      forall vn. vn -> SrcLoc -> TypeParamBase vn
TypeParamDim forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadState (Map (Namespace, Name) SrcLoc) (t m),
 MonadTypeChecker m, MonadTrans t) =>
Namespace -> Name -> SrcLoc -> t m VName
checkParamName Namespace
Term Name
pv SrcLoc
loc forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc
    checkTypeParam (TypeParamType Liftedness
l Name
pv SrcLoc
loc) =
      forall vn. Liftedness -> vn -> SrcLoc -> TypeParamBase vn
TypeParamType Liftedness
l forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadState (Map (Namespace, Name) SrcLoc) (t m),
 MonadTypeChecker m, MonadTrans t) =>
Namespace -> Name -> SrcLoc -> t m VName
checkParamName Namespace
Type Name
pv SrcLoc
loc forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
loc

-- | Construct a type argument corresponding to a type parameter.
typeParamToArg :: TypeParam -> StructTypeArg
typeParamToArg :: TypeParam -> TypeArg Size
typeParamToArg (TypeParamDim VName
v SrcLoc
ploc) =
  forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim (QualName VName -> Size
NamedSize forall a b. (a -> b) -> a -> b
$ forall v. v -> QualName v
qualName VName
v) SrcLoc
ploc
typeParamToArg (TypeParamType Liftedness
_ VName
v SrcLoc
ploc) =
  forall dim. TypeBase dim () -> SrcLoc -> TypeArg dim
TypeArgType (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar () Uniqueness
Nonunique (forall v. v -> QualName v
qualName VName
v) []) SrcLoc
ploc

-- | A type substitution may be a substitution or a yet-unknown
-- substitution (but which is certainly an overloaded primitive
-- type!).  The latter is used to remove aliases from types that are
-- yet-unknown but that we know cannot carry aliases (see issue #682).
data Subst t = Subst [TypeParam] t | PrimSubst | SizeSubst Size
  deriving (Int -> Subst t -> ShowS
forall t. Show t => Int -> Subst t -> ShowS
forall t. Show t => [Subst t] -> ShowS
forall t. Show t => Subst t -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Subst t] -> ShowS
$cshowList :: forall t. Show t => [Subst t] -> ShowS
show :: Subst t -> [Char]
$cshow :: forall t. Show t => Subst t -> [Char]
showsPrec :: Int -> Subst t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> Subst t -> ShowS
Show)

instance Pretty t => Pretty (Subst t) where
  pretty :: forall ann. Subst t -> Doc ann
pretty (Subst [] t
t) = forall a ann. Pretty a => a -> Doc ann
pretty t
t
  pretty (Subst [TypeParam]
tps t
t) = forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [TypeParam]
tps) forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty t
t
  pretty Subst t
PrimSubst = Doc ann
"#<primsubst>"
  pretty (SizeSubst Size
d) = forall a ann. Pretty a => a -> Doc ann
pretty Size
d

-- | Create a type substitution corresponding to a type binding.
substFromAbbr :: TypeBinding -> Subst StructRetType
substFromAbbr :: TypeBinding -> Subst (RetTypeBase Size ())
substFromAbbr (TypeAbbr Liftedness
_ [TypeParam]
ps RetTypeBase Size ()
rt) = forall t. [TypeParam] -> t -> Subst t
Subst [TypeParam]
ps RetTypeBase Size ()
rt

-- | Substitutions to apply in a type.
type TypeSubs = VName -> Maybe (Subst StructRetType)

instance Functor Subst where
  fmap :: forall a b. (a -> b) -> Subst a -> Subst b
fmap a -> b
f (Subst [TypeParam]
ps a
t) = forall t. [TypeParam] -> t -> Subst t
Subst [TypeParam]
ps forall a b. (a -> b) -> a -> b
$ a -> b
f a
t
  fmap a -> b
_ Subst a
PrimSubst = forall t. Subst t
PrimSubst
  fmap a -> b
_ (SizeSubst Size
v) = forall t. Size -> Subst t
SizeSubst Size
v

-- | Class of types which allow for substitution of types with no
-- annotations for type variable names.
class Substitutable a where
  applySubst :: TypeSubs -> a -> a

instance Substitutable (RetTypeBase Size ()) where
  applySubst :: TypeSubs -> RetTypeBase Size () -> RetTypeBase Size ()
applySubst TypeSubs
f (RetType [VName]
dims StructType
t) =
    let RetType [VName]
more_dims StructType
t' = forall as.
Monoid as =>
(VName -> Maybe (Subst (RetTypeBase Size as)))
-> TypeBase Size as -> RetTypeBase Size as
substTypesRet TypeSubs
f StructType
t
     in forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
dims forall a. [a] -> [a] -> [a]
++ [VName]
more_dims) StructType
t'

instance Substitutable (RetTypeBase Size Aliasing) where
  applySubst :: TypeSubs
-> RetTypeBase Size (Set Alias) -> RetTypeBase Size (Set Alias)
applySubst TypeSubs
f (RetType [VName]
dims PatType
t) =
    let RetType [VName]
more_dims PatType
t' = forall as.
Monoid as =>
(VName -> Maybe (Subst (RetTypeBase Size as)))
-> TypeBase Size as -> RetTypeBase Size as
substTypesRet VName -> Maybe (Subst (RetTypeBase Size (Set Alias)))
f' PatType
t
     in forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
dims forall a. [a] -> [a] -> [a]
++ [VName]
more_dims) PatType
t'
    where
      f' :: VName -> Maybe (Subst (RetTypeBase Size (Set Alias)))
f' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty))) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSubs
f

instance Substitutable (TypeBase Size ()) where
  applySubst :: TypeSubs -> StructType -> StructType
applySubst = forall as.
Monoid as =>
(VName -> Maybe (Subst (RetTypeBase Size as)))
-> TypeBase Size as -> TypeBase Size as
substTypesAny

instance Substitutable (TypeBase Size Aliasing) where
  applySubst :: TypeSubs -> PatType -> PatType
applySubst = forall as.
Monoid as =>
(VName -> Maybe (Subst (RetTypeBase Size as)))
-> TypeBase Size as -> TypeBase Size as
substTypesAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a b. a -> b -> a
const forall a. Monoid a => a
mempty))) .)

instance Substitutable Size where
  applySubst :: TypeSubs -> Size -> Size
applySubst TypeSubs
f (NamedSize (QualName [VName]
_ VName
v))
    | Just (SizeSubst Size
d) <- TypeSubs
f VName
v = Size
d
  applySubst TypeSubs
_ Size
d = Size
d

instance Substitutable d => Substitutable (Shape d) where
  applySubst :: TypeSubs -> Shape d -> Shape d
applySubst TypeSubs
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f

instance Substitutable Pat where
  applySubst :: TypeSubs -> Pat -> Pat
applySubst TypeSubs
f = forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x (m :: * -> *).
(ASTMappable x, Monad m) =>
ASTMapper m -> x -> m x
astMap ASTMapper Identity
mapper
    where
      mapper :: ASTMapper Identity
mapper =
        ASTMapper
          { mapOnExp :: ExpBase Info VName -> Identity (ExpBase Info VName)
mapOnExp = forall (f :: * -> *) a. Applicative f => a -> f a
pure,
            mapOnName :: VName -> Identity VName
mapOnName = forall (f :: * -> *) a. Applicative f => a -> f a
pure,
            mapOnStructType :: StructType -> Identity StructType
mapOnStructType = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f,
            mapOnPatType :: PatType -> Identity PatType
mapOnPatType = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f,
            mapOnStructRetType :: RetTypeBase Size () -> Identity (RetTypeBase Size ())
mapOnStructRetType = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f,
            mapOnPatRetType :: RetTypeBase Size (Set Alias)
-> Identity (RetTypeBase Size (Set Alias))
mapOnPatRetType = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
f
          }

applyType ::
  Monoid als =>
  [TypeParam] ->
  TypeBase Size als ->
  [StructTypeArg] ->
  TypeBase Size als
applyType :: forall als.
Monoid als =>
[TypeParam]
-> TypeBase Size als -> [TypeArg Size] -> TypeBase Size als
applyType [TypeParam]
ps TypeBase Size als
t [TypeArg Size]
args = forall as.
Monoid as =>
(VName -> Maybe (Subst (RetTypeBase Size as)))
-> TypeBase Size as -> TypeBase Size as
substTypesAny (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map VName (Subst (RetTypeBase Size als))
substs) TypeBase Size als
t
  where
    substs :: Map VName (Subst (RetTypeBase Size als))
substs = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {as} {a}.
(Monoid as, Eq a, IsName a) =>
TypeParamBase a -> TypeArg Size -> (a, Subst (RetTypeBase Size as))
mkSubst [TypeParam]
ps [TypeArg Size]
args
    -- We are assuming everything has already been type-checked for correctness.
    mkSubst :: TypeParamBase a -> TypeArg Size -> (a, Subst (RetTypeBase Size as))
mkSubst (TypeParamDim a
pv SrcLoc
_) (TypeArgDim Size
d SrcLoc
_) =
      (a
pv, forall t. Size -> Subst t
SizeSubst Size
d)
    mkSubst (TypeParamType Liftedness
_ a
pv SrcLoc
_) (TypeArgType StructType
at SrcLoc
_) =
      (a
pv, forall t. [TypeParam] -> t -> Subst t
Subst [] forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a. Monoid a => a
mempty StructType
at)
    mkSubst TypeParamBase a
p TypeArg Size
a =
      forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"applyType mkSubst: cannot substitute " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyString TypeArg Size
a forall a. [a] -> [a] -> [a]
++ [Char]
" for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyString TypeParamBase a
p

substTypesRet ::
  Monoid as =>
  (VName -> Maybe (Subst (RetTypeBase Size as))) ->
  TypeBase Size as ->
  RetTypeBase Size as
substTypesRet :: forall as.
Monoid as =>
(VName -> Maybe (Subst (RetTypeBase Size as)))
-> TypeBase Size as -> RetTypeBase Size as
substTypesRet VName -> Maybe (Subst (RetTypeBase Size as))
lookupSubst TypeBase Size as
ot =
  forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType) forall a b. (a -> b) -> a -> b
$ forall s a. State s a -> s -> (a, s)
runState (forall as.
Monoid as =>
TypeBase Size as -> State [VName] (TypeBase Size as)
onType TypeBase Size as
ot) []
  where
    -- In case we are substituting the same RetType in multiple
    -- places, we must ensure each instance is given distinct
    -- dimensions.  E.g. substituting 'a ↦ ?[n].[n]bool' into '(a,a)'
    -- should give '?[n][m].([n]bool,[m]bool)'.
    --
    -- XXX: the size names we invent here not globally unique.  This
    -- is _probably_ not a problem, since substituting types with
    -- outermost non-null existential sizes is done only when type
    -- checking modules.
    freshDims :: RetTypeBase Size as -> f (RetTypeBase Size as)
freshDims (RetType [] TypeBase Size as
t) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [] TypeBase Size as
t
    freshDims (RetType [VName]
ext TypeBase Size as
t) = do
      [VName]
seen_ext <- forall s (m :: * -> *). MonadState s m => m s
get
      if Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
seen_ext) [VName]
ext
        then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext TypeBase Size as
t
        else do
          let start :: Int
start = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map VName -> Int
baseTag [VName]
seen_ext
              ext' :: [VName]
ext' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Name -> Int -> VName
VName (forall a b. (a -> b) -> [a] -> [b]
map VName -> Name
baseName [VName]
ext) [Int
start forall a. Num a => a -> a -> a
+ Int
1 ..]
              extsubsts :: Map VName (Subst t)
extsubsts = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
ext forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t. Size -> Subst t
SizeSubst forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Size
NamedSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. v -> QualName v
qualName) [VName]
ext'
              RetType [] TypeBase Size as
t' = forall as.
Monoid as =>
(VName -> Maybe (Subst (RetTypeBase Size as)))
-> TypeBase Size as -> RetTypeBase Size as
substTypesRet (forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` forall {t}. Map VName (Subst t)
extsubsts) TypeBase Size as
t
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
ext' TypeBase Size as
t'

    onType ::
      forall as.
      Monoid as =>
      TypeBase Size as ->
      State [VName] (TypeBase Size as)

    onType :: forall as.
Monoid as =>
TypeBase Size as -> State [VName] (TypeBase Size as)
onType (Array as
als Uniqueness
u Shape Size
shape ScalarTypeBase Size ()
et) = do
      StructType
t <- forall as dim.
Monoid as =>
Uniqueness -> Shape dim -> TypeBase dim as -> TypeBase dim as
arrayOf Uniqueness
u (forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
lookupSubst' Shape Size
shape) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall as.
Monoid as =>
TypeBase Size as -> State [VName] (TypeBase Size as)
onType (forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar ScalarTypeBase Size ()
et)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ StructType
t forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` as
als
    onType (Scalar (Prim PrimType
t)) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as. PrimType -> ScalarTypeBase dim as
Prim PrimType
t
    onType (Scalar (TypeVar as
als Uniqueness
u QualName VName
v [TypeArg Size]
targs)) = do
      [TypeArg Size]
targs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {m :: * -> *}.
MonadState [VName] m =>
TypeArg Size -> m (TypeArg Size)
subsTypeArg [TypeArg Size]
targs
      case VName -> Maybe (Subst (RetTypeBase Size as))
lookupSubst forall a b. (a -> b) -> a -> b
$ forall vn. QualName vn -> vn
qualLeaf QualName VName
v of
        Just (Subst [TypeParam]
ps RetTypeBase Size as
rt) -> do
          RetType [VName]
ext TypeBase Size as
t <- forall {f :: * -> *} {as}.
(MonadState [VName] f, Monoid as) =>
RetTypeBase Size as -> f (RetTypeBase Size as)
freshDims RetTypeBase Size as
rt
          forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ([VName]
ext ++)
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
            forall als.
Monoid als =>
[TypeParam]
-> TypeBase Size als -> [TypeArg Size] -> TypeBase Size als
applyType [TypeParam]
ps (TypeBase Size as
t forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` forall a. Monoid a => a
mempty) [TypeArg Size]
targs'
              forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
u
              forall dim asf ast.
TypeBase dim asf -> (asf -> ast) -> TypeBase dim ast
`addAliases` (forall a. Semigroup a => a -> a -> a
<> as
als)
        Just Subst (RetTypeBase Size as)
PrimSubst ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar forall a. Monoid a => a
mempty Uniqueness
u QualName VName
v [TypeArg Size]
targs'
        Maybe (Subst (RetTypeBase Size as))
_ ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall a b. (a -> b) -> a -> b
$ forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar as
als Uniqueness
u QualName VName
v [TypeArg Size]
targs'
    onType (Scalar (Record Map Name (TypeBase Size as)
ts)) =
      forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall as.
Monoid as =>
TypeBase Size as -> State [VName] (TypeBase Size as)
onType Map Name (TypeBase Size as)
ts
    onType (Scalar (Arrow as
als PName
v StructType
t1 RetTypeBase Size as
t2)) =
      forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall dim as.
as
-> PName
-> TypeBase dim ()
-> RetTypeBase dim as
-> ScalarTypeBase dim as
Arrow as
als PName
v forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall as.
Monoid as =>
TypeBase Size as -> State [VName] (TypeBase Size as)
onType StructType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {f :: * -> *} {as}.
(MonadState [VName] f, Monoid as) =>
RetTypeBase Size as -> f (RetTypeBase Size as)
onRetType RetTypeBase Size as
t2)
    onType (Scalar (Sum Map Name [TypeBase Size as]
ts)) =
      forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall as.
Monoid as =>
TypeBase Size as -> State [VName] (TypeBase Size as)
onType) Map Name [TypeBase Size as]
ts

    onRetType :: RetTypeBase Size as -> m (RetTypeBase Size as)
onRetType (RetType [VName]
dims TypeBase Size as
t) = do
      [VName]
ext <- forall s (m :: * -> *). MonadState s m => m s
get
      let (TypeBase Size as
t', [VName]
ext') = forall s a. State s a -> s -> (a, s)
runState (forall as.
Monoid as =>
TypeBase Size as -> State [VName] (TypeBase Size as)
onType TypeBase Size as
t) [VName]
ext
          new_ext :: [VName]
new_ext = [VName]
ext' forall a. Eq a => [a] -> [a] -> [a]
\\ [VName]
ext
      case TypeBase Size as
t of
        Scalar Arrow {} -> do
          forall s (m :: * -> *). MonadState s m => s -> m ()
put [VName]
ext'
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType [VName]
dims TypeBase Size as
t'
        TypeBase Size as
_ ->
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
RetType ([VName]
new_ext forall a. Semigroup a => a -> a -> a
<> [VName]
dims) TypeBase Size as
t'

    subsTypeArg :: TypeArg Size -> m (TypeArg Size)
subsTypeArg (TypeArgType StructType
t SrcLoc
loc) = do
      let RetType [VName]
dims StructType
t' = forall as.
Monoid as =>
(VName -> Maybe (Subst (RetTypeBase Size as)))
-> TypeBase Size as -> RetTypeBase Size as
substTypesRet TypeSubs
lookupSubst' StructType
t
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ([VName]
dims ++)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim. TypeBase dim () -> SrcLoc -> TypeArg dim
TypeArgType StructType
t' SrcLoc
loc
    subsTypeArg (TypeArgDim Size
v SrcLoc
loc) =
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall dim. dim -> SrcLoc -> TypeArg dim
TypeArgDim (forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
lookupSubst' Size
v) SrcLoc
loc

    lookupSubst' :: TypeSubs
lookupSubst' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a b. a -> b -> a
const ())) forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> Maybe (Subst (RetTypeBase Size as))
lookupSubst

-- | Perform substitutions, from type names to types, on a type. Works
-- regardless of what shape and uniqueness information is attached to the type.
substTypesAny ::
  Monoid as =>
  (VName -> Maybe (Subst (RetTypeBase Size as))) ->
  TypeBase Size as ->
  TypeBase Size as
substTypesAny :: forall as.
Monoid as =>
(VName -> Maybe (Subst (RetTypeBase Size as)))
-> TypeBase Size as -> TypeBase Size as
substTypesAny VName -> Maybe (Subst (RetTypeBase Size as))
lookupSubst TypeBase Size as
ot =
  case forall as.
Monoid as =>
(VName -> Maybe (Subst (RetTypeBase Size as)))
-> TypeBase Size as -> RetTypeBase Size as
substTypesRet VName -> Maybe (Subst (RetTypeBase Size as))
lookupSubst TypeBase Size as
ot of
    RetType [] TypeBase Size as
ot' -> TypeBase Size as
ot'
    RetType [VName]
dims TypeBase Size as
ot' ->
      -- XXX HACK FIXME: turn any sizes that propagate to the top into
      -- AnySize.  This should _never_ happen during type-checking, but
      -- may happen as we substitute types during monomorphisation and
      -- defunctorisation later on. See Note [AnySize]
      let toAny :: Size -> Size
toAny (NamedSize QualName VName
v)
            | forall vn. QualName vn -> vn
qualLeaf QualName VName
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
dims = Maybe VName -> Size
AnySize forall a. Maybe a
Nothing
          toAny Size
d = Size
d
       in forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Size -> Size
toAny TypeBase Size as
ot'

-- Note [AnySize]
--
-- Consider a program:
--
-- module m : { type~ t } = { type~ t = ?[n].[n]bool }
-- let f (x: m.t) (y: m.t) = 0
--
-- After defunctorisation (and inlining the definitions of types), we
-- want this:
--
-- let f [n][m] (x: [n]bool) (y: [m]bool) = 0
--
-- But this means that defunctorisation would need to redo some amount
-- of size inference.  Not so complicated in the example above, but
-- what if loops and branches are involved?
--
-- So instead, what defunctorisation actually does is produce this:
--
-- let f (x: []bool) (y: []bool) = 0
--
-- I.e. we put in empty dimensions (AnySize), which are much later
-- turned into distinct sizes in Futhark.Internalise.Exps.  This will
-- result in unnecessary dynamic size checks, which will hopefully be
-- optimised away.
--
-- Important: The type checker will _never_ produce programs with
-- AnySize, but unfortunately some of the compilation steps
-- (defunctorisation, monomorphisation, defunctionalisation) will do
-- so.  Similarly, the core language is also perfectly well behaved.
--
-- Example with monomorphisation:
--
-- let f '~a (b: bool) (x: () -> a) (y: () -> a) : a = if b then x () else y ()
-- let g = f true (\() -> [1]) (\() -> [1,2])
--
-- This should produce:
--
-- let f (b: bool) (x: () -> ?[n].[n]i32) (y: () -> ?[m].[m]i32) : ?[k].[k]i32 =
--   if b then x () else y ()
--
-- Not so easy!  Again, what we actually produce is
--
-- let f (b: bool) (x: () -> []i32) (y: () -> []i32) : []i32 =
--   if b then x () else y ()