-- | Type inference of @loop@.  This is complicated because of the
-- uniqueness and size inference, so the implementation is separate
-- from the main type checker.
module Language.Futhark.TypeChecker.Terms.DoLoop
  ( UncheckedLoop,
    CheckedLoop,
    checkDoLoop,
  )
where

import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Data.Bifunctor
import Data.Bitraversable
import Data.Map.Strict qualified as M
import Data.Maybe
import Data.Set qualified as S
import Futhark.Util (nubOrd)
import Futhark.Util.Pretty hiding (group, space)
import Language.Futhark
import Language.Futhark.TypeChecker.Monad hiding (BoundV)
import Language.Futhark.TypeChecker.Terms.Monad hiding (consumed)
import Language.Futhark.TypeChecker.Terms.Pat
import Language.Futhark.TypeChecker.Types
import Language.Futhark.TypeChecker.Unify
import Prelude hiding (mod)

-- | Replace specified sizes with distinct fresh size variables.
someDimsFreshInType ::
  SrcLoc ->
  Rigidity ->
  Name ->
  S.Set VName ->
  TypeBase Size als ->
  TermTypeM (TypeBase Size als)
someDimsFreshInType :: forall als.
SrcLoc
-> Rigidity
-> Name
-> Names
-> TypeBase Size als
-> TermTypeM (TypeBase Size als)
someDimsFreshInType SrcLoc
loc Rigidity
r Name
desc Names
sizes = forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse forall {m :: * -> *}. MonadUnify m => Size -> m Size
onDim forall (f :: * -> *) a. Applicative f => a -> f a
pure
  where
    onDim :: Size -> m Size
onDim (NamedSize QualName VName
d)
      | forall vn. QualName vn -> vn
qualLeaf QualName VName
d forall a. Ord a => a -> Set a -> Bool
`S.member` Names
sizes = do
          VName
v <- forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc Rigidity
r Name
desc
          forall (f :: * -> *) a. Applicative f => a -> f a
pure 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
v
    onDim Size
d = forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
d

-- | Replace the specified sizes with fresh size variables of the
-- specified ridigity.  Returns the new fresh size variables.
freshDimsInType ::
  SrcLoc ->
  Rigidity ->
  Name ->
  S.Set VName ->
  TypeBase Size als ->
  TermTypeM (TypeBase Size als, [VName])
freshDimsInType :: forall als.
SrcLoc
-> Rigidity
-> Name
-> Names
-> TypeBase Size als
-> TermTypeM (TypeBase Size als, [VName])
freshDimsInType SrcLoc
loc Rigidity
r Name
desc Names
sizes TypeBase Size als
t =
  forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall k a. Map k a -> [a]
M.elems forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse forall {t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadState (Map VName VName) (t m), MonadTrans t, MonadUnify m) =>
Size -> t m Size
onDim forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeBase Size als
t) forall a. Monoid a => a
mempty
  where
    onDim :: Size -> t m Size
onDim (NamedSize QualName VName
d)
      | forall vn. QualName vn -> vn
qualLeaf QualName VName
d forall a. Ord a => a -> Set a -> Bool
`S.member` Names
sizes = do
          Maybe VName
prev_subst <- 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 forall a b. (a -> b) -> a -> b
$ forall vn. QualName vn -> vn
qualLeaf QualName VName
d
          case Maybe VName
prev_subst of
            Just VName
d' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure 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'
            Maybe VName
Nothing -> do
              VName
v <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc Rigidity
r Name
desc
              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 (forall vn. QualName vn -> vn
qualLeaf QualName VName
d) VName
v
              forall (f :: * -> *) a. Applicative f => a -> f a
pure 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
v
    onDim Size
d = forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
d

-- | Mark bindings of names in "consumed" as Unique.
uniquePat :: Names -> Pat -> Pat
uniquePat :: Names -> Pat -> Pat
uniquePat Names
consumed = Pat -> Pat
recurse
  where
    recurse :: Pat -> Pat
recurse (Wildcard (Info PatType
t) SrcLoc
wloc) =
      forall (f :: * -> *) vn. f PatType -> SrcLoc -> PatBase f vn
Wildcard (forall a. a -> Info a
Info forall a b. (a -> b) -> a -> b
$ PatType
t forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
Nonunique) SrcLoc
wloc
    recurse (PatParens Pat
p SrcLoc
ploc) =
      forall (f :: * -> *) vn. PatBase f vn -> SrcLoc -> PatBase f vn
PatParens (Pat -> Pat
recurse Pat
p) SrcLoc
ploc
    recurse (PatAttr AttrInfo VName
attr Pat
p SrcLoc
ploc) =
      forall (f :: * -> *) vn.
AttrInfo vn -> PatBase f vn -> SrcLoc -> PatBase f vn
PatAttr AttrInfo VName
attr (Pat -> Pat
recurse Pat
p) SrcLoc
ploc
    recurse (Id VName
name (Info PatType
t) SrcLoc
iloc)
      | VName
name forall a. Ord a => a -> Set a -> Bool
`S.member` Names
consumed =
          let t' :: PatType
t' = PatType
t forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
Unique forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` forall a. Monoid a => a
mempty
           in forall (f :: * -> *) vn. vn -> f PatType -> SrcLoc -> PatBase f vn
Id VName
name (forall a. a -> Info a
Info PatType
t') SrcLoc
iloc
      | Bool
otherwise =
          let t' :: PatType
t' = PatType
t forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
Nonunique
           in forall (f :: * -> *) vn. vn -> f PatType -> SrcLoc -> PatBase f vn
Id VName
name (forall a. a -> Info a
Info PatType
t') SrcLoc
iloc
    recurse (TuplePat [Pat]
pats SrcLoc
ploc) =
      forall (f :: * -> *) vn. [PatBase f vn] -> SrcLoc -> PatBase f vn
TuplePat (forall a b. (a -> b) -> [a] -> [b]
map Pat -> Pat
recurse [Pat]
pats) SrcLoc
ploc
    recurse (RecordPat [(Name, Pat)]
fs SrcLoc
ploc) =
      forall (f :: * -> *) vn.
[(Name, PatBase f vn)] -> SrcLoc -> PatBase f vn
RecordPat (forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pat -> Pat
recurse) [(Name, Pat)]
fs) SrcLoc
ploc
    recurse (PatAscription Pat
p TypeExp VName
t SrcLoc
ploc) =
      forall (f :: * -> *) vn.
PatBase f vn -> TypeExp vn -> SrcLoc -> PatBase f vn
PatAscription Pat
p TypeExp VName
t SrcLoc
ploc
    recurse p :: Pat
p@PatLit {} = Pat
p
    recurse (PatConstr Name
n Info PatType
t [Pat]
ps SrcLoc
ploc) =
      forall (f :: * -> *) vn.
Name -> f PatType -> [PatBase f vn] -> SrcLoc -> PatBase f vn
PatConstr Name
n Info PatType
t (forall a b. (a -> b) -> [a] -> [b]
map Pat -> Pat
recurse [Pat]
ps) SrcLoc
ploc

convergePat :: SrcLoc -> Pat -> Names -> PatType -> Usage -> TermTypeM Pat
convergePat :: SrcLoc -> Pat -> Names -> PatType -> Usage -> TermTypeM Pat
convergePat SrcLoc
loop_loc Pat
pat Names
body_cons PatType
body_t Usage
body_loc = do
  let -- Make the pattern unique where needed.
      pat' :: Pat
pat' = Names -> Pat -> Pat
uniquePat (forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set vn
patNames Pat
pat forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` Names
body_cons) Pat
pat

  -- Check that the new values of consumed merge parameters do not
  -- alias something bound outside the loop, AND that anything
  -- returned for a unique merge parameter does not alias anything
  -- else returned.  We also update the aliases for the pattern.
  Names
bound_outside <- forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ 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 b c a. (b -> c) -> (a -> b) -> a -> c
. TermScope -> Map VName ValBinding
scopeVtable forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermEnv -> TermScope
termScope
  let combAliases :: TypeBase dim asf -> TypeBase shape asf -> TypeBase dim asf
combAliases TypeBase dim asf
t1 TypeBase shape asf
t2 =
        case TypeBase dim asf
t1 of
          Scalar Record {} -> TypeBase dim asf
t1
          TypeBase dim asf
_ -> TypeBase dim asf
t1 forall dim asf ast.
TypeBase dim asf -> (asf -> ast) -> TypeBase dim ast
`addAliases` (forall a. Semigroup a => a -> a -> a
<> forall as shape. Monoid as => TypeBase shape as -> as
aliases TypeBase shape asf
t2)

      checkMergeReturn :: PatBase Info vn
-> TypeBase dim (Set Alias) -> t m (PatBase Info vn)
checkMergeReturn (Id vn
pat_v (Info PatType
pat_v_t) SrcLoc
patloc) TypeBase dim (Set Alias)
t
        | forall shape as. TypeBase shape as -> Bool
unique PatType
pat_v_t,
          VName
v : [VName]
_ <-
            forall a. Set a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$
              forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Alias -> VName
aliasVar (forall as shape. Monoid as => TypeBase shape as -> as
aliases TypeBase dim (Set Alias)
t) forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` Names
bound_outside =
            forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loop_loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
              Doc ()
"Return value for loop parameter"
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName vn
pat_v)
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"aliases"
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName VName
v) forall a. Semigroup a => a -> a -> a
<> Doc ()
"."
        | Bool
otherwise = do
            (Set Alias
cons, Set Alias
obs) <- forall s (m :: * -> *). MonadState s m => m s
get
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Set a -> Bool
S.null forall a b. (a -> b) -> a -> b
$ forall as shape. Monoid as => TypeBase shape as -> as
aliases TypeBase dim (Set Alias)
t forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` Set Alias
cons) forall a b. (a -> b) -> a -> b
$
              forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loop_loc forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
                Doc ()
"Return value for loop parameter"
                  forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName vn
pat_v)
                  forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"aliases other consumed loop parameter."
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
              ( forall shape as. TypeBase shape as -> Bool
unique PatType
pat_v_t
                  Bool -> Bool -> Bool
&& Bool -> Bool
not (forall a. Set a -> Bool
S.null (forall as shape. Monoid as => TypeBase shape as -> as
aliases TypeBase dim (Set Alias)
t forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` (Set Alias
cons forall a. Semigroup a => a -> a -> a
<> Set Alias
obs)))
              )
              forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError SrcLoc
loop_loc forall a. Monoid a => a
mempty
              forall a b. (a -> b) -> a -> b
$ Doc ()
"Return value for consuming loop parameter"
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann -> Doc ann
dquotes (forall v a. IsName v => v -> Doc a
prettyName vn
pat_v)
                forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"aliases previously returned value."
            if forall shape as. TypeBase shape as -> Bool
unique PatType
pat_v_t
              then forall s (m :: * -> *). MonadState s m => s -> m ()
put (Set Alias
cons forall a. Semigroup a => a -> a -> a
<> forall as shape. Monoid as => TypeBase shape as -> as
aliases TypeBase dim (Set Alias)
t, Set Alias
obs)
              else forall s (m :: * -> *). MonadState s m => s -> m ()
put (Set Alias
cons, Set Alias
obs forall a. Semigroup a => a -> a -> a
<> forall as shape. Monoid as => TypeBase shape as -> as
aliases TypeBase dim (Set Alias)
t)

            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. vn -> f PatType -> SrcLoc -> PatBase f vn
Id vn
pat_v (forall a. a -> Info a
Info (forall {asf} {dim} {shape}.
Monoid asf =>
TypeBase dim asf -> TypeBase shape asf -> TypeBase dim asf
combAliases PatType
pat_v_t TypeBase dim (Set Alias)
t)) SrcLoc
patloc
      checkMergeReturn (Wildcard (Info PatType
pat_v_t) SrcLoc
patloc) TypeBase dim (Set Alias)
t =
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. f PatType -> SrcLoc -> PatBase f vn
Wildcard (forall a. a -> Info a
Info (forall {asf} {dim} {shape}.
Monoid asf =>
TypeBase dim asf -> TypeBase shape asf -> TypeBase dim asf
combAliases PatType
pat_v_t TypeBase dim (Set Alias)
t)) SrcLoc
patloc
      checkMergeReturn (PatParens PatBase Info vn
p SrcLoc
_) TypeBase dim (Set Alias)
t =
        PatBase Info vn
-> TypeBase dim (Set Alias) -> t m (PatBase Info vn)
checkMergeReturn PatBase Info vn
p TypeBase dim (Set Alias)
t
      checkMergeReturn (PatAscription PatBase Info vn
p TypeExp vn
_ SrcLoc
_) TypeBase dim (Set Alias)
t =
        PatBase Info vn
-> TypeBase dim (Set Alias) -> t m (PatBase Info vn)
checkMergeReturn PatBase Info vn
p TypeBase dim (Set Alias)
t
      checkMergeReturn (RecordPat [(Name, PatBase Info vn)]
pfs SrcLoc
patloc) (Scalar (Record Map Name (TypeBase dim (Set Alias))
tfs)) =
        forall (f :: * -> *) vn.
[(Name, PatBase f vn)] -> SrcLoc -> PatBase f vn
RecordPat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
M.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence Map Name (t m (PatBase Info vn))
pfs' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
patloc
        where
          pfs' :: Map Name (t m (PatBase Info vn))
pfs' = forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
M.intersectionWith PatBase Info vn
-> TypeBase dim (Set Alias) -> t m (PatBase Info vn)
checkMergeReturn (forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name, PatBase Info vn)]
pfs) Map Name (TypeBase dim (Set Alias))
tfs
      checkMergeReturn (TuplePat [PatBase Info vn]
pats SrcLoc
patloc) TypeBase dim (Set Alias)
t
        | Just [TypeBase dim (Set Alias)]
ts <- forall dim as. TypeBase dim as -> Maybe [TypeBase dim as]
isTupleRecord TypeBase dim (Set Alias)
t =
            forall (f :: * -> *) vn. [PatBase f vn] -> SrcLoc -> PatBase f vn
TuplePat 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 PatBase Info vn
-> TypeBase dim (Set Alias) -> t m (PatBase Info vn)
checkMergeReturn [PatBase Info vn]
pats [TypeBase dim (Set Alias)]
ts forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure SrcLoc
patloc
      checkMergeReturn PatBase Info vn
p TypeBase dim (Set Alias)
_ =
        forall (f :: * -> *) a. Applicative f => a -> f a
pure PatBase Info vn
p

  (Pat
pat'', (Set Alias
pat_cons, Set Alias
_)) <-
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall {t :: (* -> *) -> * -> *} {m :: * -> *} {vn} {dim}.
(MonadTrans t, MonadTypeChecker m, IsName vn,
 MonadState (Set Alias, Set Alias) (t m)) =>
PatBase Info vn
-> TypeBase dim (Set Alias) -> t m (PatBase Info vn)
checkMergeReturn Pat
pat' PatType
body_t) (forall a. Monoid a => a
mempty, forall a. Monoid a => a
mempty)

  let body_cons' :: Names
body_cons' = Names
body_cons forall a. Semigroup a => a -> a -> a
<> forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map Alias -> VName
aliasVar Set Alias
pat_cons
  if Names
body_cons' forall a. Eq a => a -> a -> Bool
== Names
body_cons Bool -> Bool -> Bool
&& Pat -> PatType
patternType Pat
pat'' forall a. Eq a => a -> a -> Bool
== Pat -> PatType
patternType Pat
pat
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure Pat
pat'
    else SrcLoc -> Pat -> Names -> PatType -> Usage -> TermTypeM Pat
convergePat SrcLoc
loop_loc Pat
pat'' Names
body_cons' PatType
body_t Usage
body_loc

data ArgSource = Initial | BodyResult

wellTypedLoopArg :: ArgSource -> [VName] -> Pat -> Exp -> TermTypeM ()
wellTypedLoopArg :: ArgSource -> [VName] -> Pat -> Exp -> TermTypeM ()
wellTypedLoopArg ArgSource
src [VName]
sparams Pat
pat Exp
arg = do
  (TypeBase Size ()
merge_t, [VName]
_) <-
    forall als.
SrcLoc
-> Rigidity
-> Name
-> Names
-> TypeBase Size als
-> TermTypeM (TypeBase Size als, [VName])
freshDimsInType (forall a. Located a => a -> SrcLoc
srclocOf Exp
arg) Rigidity
Nonrigid Name
"loop" (forall a. Ord a => [a] -> Set a
S.fromList [VName]
sparams) forall a b. (a -> b) -> a -> b
$
      forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall a b. (a -> b) -> a -> b
$
        Pat -> PatType
patternType Pat
pat
  TypeBase Size ()
arg_t <- forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> TermTypeM PatType
expTypeFully Exp
arg
  forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (TypeBase Size () -> TypeBase Size () -> Checking
checking TypeBase Size ()
merge_t TypeBase Size ()
arg_t) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
unify
      (SrcLoc -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf Exp
arg) Text
desc)
      TypeBase Size ()
merge_t
      TypeBase Size ()
arg_t
  where
    (TypeBase Size () -> TypeBase Size () -> Checking
checking, Text
desc) =
      case ArgSource
src of
        ArgSource
Initial -> (TypeBase Size () -> TypeBase Size () -> Checking
CheckingLoopInitial, Text
"matching initial loop values to pattern")
        ArgSource
BodyResult -> (TypeBase Size () -> TypeBase Size () -> Checking
CheckingLoopBody, Text
"matching loop body to pattern")

-- | An un-checked loop.
type UncheckedLoop =
  (UncheckedPat, UncheckedExp, LoopFormBase NoInfo Name, UncheckedExp)

-- | A loop that has been type-checked.
type CheckedLoop =
  ([VName], Pat, Exp, LoopFormBase Info VName, Exp)

-- | Type-check a @loop@ expression, passing in a function for
-- type-checking subexpressions.
checkDoLoop ::
  (UncheckedExp -> TermTypeM Exp) ->
  UncheckedLoop ->
  SrcLoc ->
  TermTypeM (CheckedLoop, AppRes)
checkDoLoop :: (UncheckedExp -> TermTypeM Exp)
-> UncheckedLoop -> SrcLoc -> TermTypeM (CheckedLoop, AppRes)
checkDoLoop UncheckedExp -> TermTypeM Exp
checkExp (UncheckedPat
mergepat, UncheckedExp
mergeexp, LoopFormBase NoInfo Name
form, UncheckedExp
loopbody) SrcLoc
loc =
  forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially (UncheckedExp -> TermTypeM Exp
checkExp UncheckedExp
mergeexp) forall a b. (a -> b) -> a -> b
$ \Exp
mergeexp' Occurrences
_ -> do
    forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> Text -> TypeBase dim as -> m ()
zeroOrderType
      (SrcLoc -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf UncheckedExp
mergeexp) Text
"use as loop variable")
      Text
"type used as loop variable"
      forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expTypeFully Exp
mergeexp'

    -- The handling of dimension sizes is a bit intricate, but very
    -- similar to checking a function, followed by checking a call to
    -- it.  The overall procedure is as follows:
    --
    -- (1) All empty dimensions in the merge pattern are instantiated
    -- with nonrigid size variables.  All explicitly specified
    -- dimensions are preserved.
    --
    -- (2) The body of the loop is type-checked.  The result type is
    -- combined with the merge pattern type to determine which sizes are
    -- variant, and these are turned into size parameters for the merge
    -- pattern.
    --
    -- (3) We now conceptually have a function parameter type and
    -- return type.  We check that it can be called with the body type
    -- as argument.
    --
    -- (4) Similarly to (3), we check that the "function" can be
    -- called with the initial merge values as argument.  The result
    -- of this is the type of the loop as a whole.
    --
    -- (There is also a convergence loop for inferring uniqueness, but
    -- that's orthogonal to the size handling.)

    (PatType
merge_t, Map VName Size
new_dims_to_initial_dim) <-
      -- dim handling (1)
      forall als.
SrcLoc
-> Rigidity
-> Name
-> TypeBase Size als
-> TermTypeM (TypeBase Size als, Map VName Size)
allDimsFreshInType SrcLoc
loc Rigidity
Nonrigid Name
"loop" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expTypeFully Exp
mergeexp'
    let new_dims :: [VName]
new_dims = forall k a. Map k a -> [k]
M.keys Map VName Size
new_dims_to_initial_dim

    -- dim handling (2)
    let checkLoopReturnSize :: Pat -> Exp -> TermTypeM ([VName], Pat)
checkLoopReturnSize Pat
mergepat' Exp
loopbody' = do
          PatType
loopbody_t <- Exp -> TermTypeM PatType
expTypeFully Exp
loopbody'
          PatType
pat_t <-
            forall als.
SrcLoc
-> Rigidity
-> Name
-> Names
-> TypeBase Size als
-> TermTypeM (TypeBase Size als)
someDimsFreshInType SrcLoc
loc Rigidity
Nonrigid Name
"loop" (forall a. Ord a => [a] -> Set a
S.fromList [VName]
new_dims)
              forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully (Pat -> PatType
patternType Pat
mergepat')

          -- We are ignoring the dimensions here, because any mismatches
          -- should be turned into fresh size variables.
          forall a. Checking -> TermTypeM a -> TermTypeM a
onFailure (TypeBase Size () -> TypeBase Size () -> Checking
CheckingLoopBody (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
pat_t) (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
loopbody_t)) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *).
MonadUnify m =>
Usage -> TypeBase Size () -> TypeBase Size () -> m ()
unify
              (SrcLoc -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf UncheckedExp
loopbody) Text
"matching loop body to loop pattern")
              (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
pat_t)
              (forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
loopbody_t)

          -- Figure out which of the 'new_dims' dimensions are variant.
          -- This works because we know that each dimension from
          -- new_dims in the pattern is unique and distinct.
          let onDims :: p -> Size -> Size -> f Size
onDims p
_ Size
x Size
y
                | Size
x forall a. Eq a => a -> a -> Bool
== Size
y = forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
x
              onDims p
_ (NamedSize QualName VName
v) Size
d
                | forall vn. QualName vn -> vn
qualLeaf QualName VName
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
new_dims = do
                    case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (forall vn. QualName vn -> vn
qualLeaf QualName VName
v) Map VName Size
new_dims_to_initial_dim of
                      Just Size
d'
                        | Size
d' forall a. Eq a => a -> a -> Bool
== Size
d ->
                            forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (forall vn. QualName vn -> vn
qualLeaf QualName VName
v) (forall t. Size -> Subst t
SizeSubst Size
d)
                      Maybe Size
_ ->
                        forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall vn. QualName vn -> vn
qualLeaf QualName VName
v :)
                    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize QualName VName
v
              onDims p
_ Size
x Size
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
x
          PatType
loopbody_t' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
loopbody_t
          PatType
merge_t' <- forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
merge_t
          let (Map VName (Subst t)
init_substs, [VName]
sparams) =
                forall s a. State s a -> s -> s
execState (forall as (m :: * -> *) d1 d2.
(Monoid as, Monad m) =>
([VName] -> d1 -> d2 -> m d1)
-> TypeBase d1 as -> TypeBase d2 as -> m (TypeBase d1 as)
matchDims forall {f :: * -> *} {p :: * -> * -> *} {t} {p}.
(Bifunctor p, MonadState (p (Map VName (Subst t)) [VName]) f) =>
p -> Size -> Size -> f Size
onDims PatType
merge_t' PatType
loopbody_t') forall a. Monoid a => a
mempty

          -- Make sure that any of new_dims that are invariant will be
          -- replaced with the invariant size in the loop body.  Failure
          -- to do this can cause type annotations to still refer to
          -- new_dims.
          let dimToInit :: (VName, Subst t) -> TermTypeM ()
dimToInit (VName
v, SizeSubst Size
d) =
                VName -> Constraint -> TermTypeM ()
constrain VName
v forall a b. (a -> b) -> a -> b
$ Maybe Size -> Usage -> Constraint
Size (forall a. a -> Maybe a
Just Size
d) (SrcLoc -> Text -> Usage
mkUsage SrcLoc
loc Text
"size of loop parameter")
              dimToInit (VName, Subst t)
_ =
                forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {t}. (VName, Subst t) -> TermTypeM ()
dimToInit forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList forall {t}. Map VName (Subst t)
init_substs

          Pat
mergepat'' <- 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)
init_substs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e. ASTMappable e => e -> TermTypeM e
updateTypes Pat
mergepat'

          -- Eliminate those new_dims that turned into sparams so it won't
          -- look like we have ambiguous sizes lying around.
          forall (m :: * -> *).
MonadUnify m =>
(Constraints -> Constraints) -> m ()
modifyConstraints forall a b. (a -> b) -> a -> b
$ forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey forall a b. (a -> b) -> a -> b
$ \VName
k (Level, Constraint)
_ -> VName
k forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [VName]
sparams

          -- dim handling (3)
          --
          -- The only trick here is that we have to turn any instances
          -- of loop parameters in the type of loopbody' rigid,
          -- because we are no longer in a position to change them,
          -- really.
          ArgSource -> [VName] -> Pat -> Exp -> TermTypeM ()
wellTypedLoopArg ArgSource
BodyResult [VName]
sparams Pat
mergepat'' Exp
loopbody'

          forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Ord a => [a] -> [a]
nubOrd [VName]
sparams, Pat
mergepat'')

    -- First we do a basic check of the loop body to figure out which of
    -- the merge parameters are being consumed.  For this, we first need
    -- to check the merge pattern, which requires the (initial) merge
    -- expression.
    --
    -- Play a little with occurences to ensure it does not look like
    -- none of the merge variables are being used.
    (([VName]
sparams, Pat
mergepat', LoopFormBase Info VName
form', Exp
loopbody'), Occurrences
bodyflow) <-
      case LoopFormBase NoInfo Name
form of
        For IdentBase NoInfo Name
i UncheckedExp
uboundexp -> do
          Exp
uboundexp' <-
            Text -> [PrimType] -> Exp -> TermTypeM Exp
require Text
"being the bound in a 'for' loop" [PrimType]
anySignedType
              forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< UncheckedExp -> TermTypeM Exp
checkExp UncheckedExp
uboundexp
          PatType
bound_t <- Exp -> TermTypeM PatType
expTypeFully Exp
uboundexp'
          forall a.
IdentBase NoInfo Name
-> PatType -> (Ident -> TermTypeM a) -> TermTypeM a
bindingIdent IdentBase NoInfo Name
i PatType
bound_t forall a b. (a -> b) -> a -> b
$ \Ident
i' ->
            forall a. TermTypeM a -> TermTypeM a
noUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
[SizeBinder VName]
-> UncheckedPat
-> InferredType
-> (Pat -> TermTypeM a)
-> TermTypeM a
bindingPat [] UncheckedPat
mergepat (PatType -> InferredType
Ascribed PatType
merge_t) forall a b. (a -> b) -> a -> b
$
              \Pat
mergepat' -> forall a. TermTypeM a -> TermTypeM a
onlySelfAliasing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TermTypeM a -> TermTypeM (a, Occurrences)
tapOccurrences forall a b. (a -> b) -> a -> b
$ do
                Exp
loopbody' <- forall a. TermTypeM a -> TermTypeM a
noSizeEscape forall a b. (a -> b) -> a -> b
$ UncheckedExp -> TermTypeM Exp
checkExp UncheckedExp
loopbody
                ([VName]
sparams, Pat
mergepat'') <- Pat -> Exp -> TermTypeM ([VName], Pat)
checkLoopReturnSize Pat
mergepat' Exp
loopbody'
                forall (f :: * -> *) a. Applicative f => a -> f a
pure
                  ( [VName]
sparams,
                    Pat
mergepat'',
                    forall (f :: * -> *) vn.
IdentBase f vn -> ExpBase f vn -> LoopFormBase f vn
For Ident
i' Exp
uboundexp',
                    Exp
loopbody'
                  )
        ForIn UncheckedPat
xpat UncheckedExp
e -> do
          (TypeBase Size ()
arr_t, TypeBase Size ()
_) <- SrcLoc
-> Name -> Level -> TermTypeM (TypeBase Size (), TypeBase Size ())
newArrayType (forall a. Located a => a -> SrcLoc
srclocOf UncheckedExp
e) Name
"e" Level
1
          Exp
e' <- Text -> TypeBase Size () -> Exp -> TermTypeM Exp
unifies Text
"being iterated in a 'for-in' loop" TypeBase Size ()
arr_t forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< UncheckedExp -> TermTypeM Exp
checkExp UncheckedExp
e
          PatType
t <- Exp -> TermTypeM PatType
expTypeFully Exp
e'
          case PatType
t of
            PatType
_
              | Just PatType
t' <- forall dim as. Level -> TypeBase dim as -> Maybe (TypeBase dim as)
peelArray Level
1 PatType
t ->
                  forall a.
[SizeBinder VName]
-> UncheckedPat
-> InferredType
-> (Pat -> TermTypeM a)
-> TermTypeM a
bindingPat [] UncheckedPat
xpat (PatType -> InferredType
Ascribed PatType
t') forall a b. (a -> b) -> a -> b
$ \Pat
xpat' ->
                    forall a. TermTypeM a -> TermTypeM a
noUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
[SizeBinder VName]
-> UncheckedPat
-> InferredType
-> (Pat -> TermTypeM a)
-> TermTypeM a
bindingPat [] UncheckedPat
mergepat (PatType -> InferredType
Ascribed PatType
merge_t) forall a b. (a -> b) -> a -> b
$
                      \Pat
mergepat' -> forall a. TermTypeM a -> TermTypeM a
onlySelfAliasing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TermTypeM a -> TermTypeM (a, Occurrences)
tapOccurrences forall a b. (a -> b) -> a -> b
$ do
                        Exp
loopbody' <- forall a. TermTypeM a -> TermTypeM a
noSizeEscape forall a b. (a -> b) -> a -> b
$ UncheckedExp -> TermTypeM Exp
checkExp UncheckedExp
loopbody
                        ([VName]
sparams, Pat
mergepat'') <- Pat -> Exp -> TermTypeM ([VName], Pat)
checkLoopReturnSize Pat
mergepat' Exp
loopbody'
                        forall (f :: * -> *) a. Applicative f => a -> f a
pure
                          ( [VName]
sparams,
                            Pat
mergepat'',
                            forall (f :: * -> *) vn.
PatBase f vn -> ExpBase f vn -> LoopFormBase f vn
ForIn Pat
xpat' Exp
e',
                            Exp
loopbody'
                          )
              | Bool
otherwise ->
                  forall (m :: * -> *) loc a.
(MonadTypeChecker m, Located loc) =>
loc -> Notes -> Doc () -> m a
typeError (forall a. Located a => a -> SrcLoc
srclocOf UncheckedExp
e) forall a. Monoid a => a
mempty forall a b. (a -> b) -> a -> b
$
                    Doc ()
"Iteratee of a for-in loop must be an array, but expression has type"
                      forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty PatType
t
        While UncheckedExp
cond ->
          forall a. TermTypeM a -> TermTypeM a
noUnique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
[SizeBinder VName]
-> UncheckedPat
-> InferredType
-> (Pat -> TermTypeM a)
-> TermTypeM a
bindingPat [] UncheckedPat
mergepat (PatType -> InferredType
Ascribed PatType
merge_t) forall a b. (a -> b) -> a -> b
$ \Pat
mergepat' ->
            forall a. TermTypeM a -> TermTypeM a
onlySelfAliasing
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TermTypeM a -> TermTypeM (a, Occurrences)
tapOccurrences
              forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b.
TermTypeM a -> (a -> Occurrences -> TermTypeM b) -> TermTypeM b
sequentially
                ( UncheckedExp -> TermTypeM Exp
checkExp UncheckedExp
cond
                    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Text -> TypeBase Size () -> Exp -> TermTypeM Exp
unifies Text
"being the condition of a 'while' loop" (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
Bool)
                )
              forall a b. (a -> b) -> a -> b
$ \Exp
cond' Occurrences
_ -> do
                Exp
loopbody' <- forall a. TermTypeM a -> TermTypeM a
noSizeEscape forall a b. (a -> b) -> a -> b
$ UncheckedExp -> TermTypeM Exp
checkExp UncheckedExp
loopbody
                ([VName]
sparams, Pat
mergepat'') <- Pat -> Exp -> TermTypeM ([VName], Pat)
checkLoopReturnSize Pat
mergepat' Exp
loopbody'
                forall (f :: * -> *) a. Applicative f => a -> f a
pure
                  ( [VName]
sparams,
                    Pat
mergepat'',
                    forall (f :: * -> *) vn. ExpBase f vn -> LoopFormBase f vn
While Exp
cond',
                    Exp
loopbody'
                  )

    Pat
mergepat'' <- do
      PatType
loopbody_t <- Exp -> TermTypeM PatType
expTypeFully Exp
loopbody'
      SrcLoc -> Pat -> Names -> PatType -> Usage -> TermTypeM Pat
convergePat SrcLoc
loc Pat
mergepat' (Occurrences -> Names
allConsumed Occurrences
bodyflow) PatType
loopbody_t forall a b. (a -> b) -> a -> b
$
        SrcLoc -> Text -> Usage
mkUsage (forall a. Located a => a -> SrcLoc
srclocOf Exp
loopbody') Text
"being (part of) the result of the loop body"

    let consumeMerge :: PatBase Info vn -> TypeBase dim (Set Alias) -> TermTypeM ()
consumeMerge (Id vn
_ (Info PatType
pt) SrcLoc
ploc) TypeBase dim (Set Alias)
mt
          | forall shape as. TypeBase shape as -> Bool
unique PatType
pt = SrcLoc -> Set Alias -> TermTypeM ()
consume SrcLoc
ploc forall a b. (a -> b) -> a -> b
$ forall as shape. Monoid as => TypeBase shape as -> as
aliases TypeBase dim (Set Alias)
mt
        consumeMerge (TuplePat [PatBase Info vn]
pats SrcLoc
_) TypeBase dim (Set Alias)
t
          | Just [TypeBase dim (Set Alias)]
ts <- forall dim as. TypeBase dim as -> Maybe [TypeBase dim as]
isTupleRecord TypeBase dim (Set Alias)
t =
              forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ PatBase Info vn -> TypeBase dim (Set Alias) -> TermTypeM ()
consumeMerge [PatBase Info vn]
pats [TypeBase dim (Set Alias)]
ts
        consumeMerge (PatParens PatBase Info vn
pat SrcLoc
_) TypeBase dim (Set Alias)
t =
          PatBase Info vn -> TypeBase dim (Set Alias) -> TermTypeM ()
consumeMerge PatBase Info vn
pat TypeBase dim (Set Alias)
t
        consumeMerge (PatAscription PatBase Info vn
pat TypeExp vn
_ SrcLoc
_) TypeBase dim (Set Alias)
t =
          PatBase Info vn -> TypeBase dim (Set Alias) -> TermTypeM ()
consumeMerge PatBase Info vn
pat TypeBase dim (Set Alias)
t
        consumeMerge PatBase Info vn
_ TypeBase dim (Set Alias)
_ =
          forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    forall {vn} {dim}.
PatBase Info vn -> TypeBase dim (Set Alias) -> TermTypeM ()
consumeMerge Pat
mergepat'' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Exp -> TermTypeM PatType
expTypeFully Exp
mergeexp'

    -- dim handling (4)
    ArgSource -> [VName] -> Pat -> Exp -> TermTypeM ()
wellTypedLoopArg ArgSource
Initial [VName]
sparams Pat
mergepat'' Exp
mergeexp'

    (PatType
loopt, [VName]
retext) <-
      forall als.
SrcLoc
-> Rigidity
-> Name
-> Names
-> TypeBase Size als
-> TermTypeM (TypeBase Size als, [VName])
freshDimsInType SrcLoc
loc (RigidSource -> Rigidity
Rigid RigidSource
RigidLoop) Name
"loop" (forall a. Ord a => [a] -> Set a
S.fromList [VName]
sparams) forall a b. (a -> b) -> a -> b
$
        Pat -> PatType
patternType Pat
mergepat''
    -- We set all of the uniqueness to be unique.  This is intentional,
    -- and matches what happens for function calls.  Those arrays that
    -- really *cannot* be consumed will alias something unconsumable,
    -- and will be caught that way.
    let bound_here :: Names
bound_here = forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set vn
patNames Pat
mergepat'' forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => [a] -> Set a
S.fromList [VName]
sparams forall a. Semigroup a => a -> a -> a
<> Names
form_bound
        form_bound :: Names
form_bound =
          case LoopFormBase Info VName
form' of
            For Ident
v Exp
_ -> forall a. a -> Set a
S.singleton forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) vn. IdentBase f vn -> vn
identName Ident
v
            ForIn Pat
forpat Exp
_ -> forall (f :: * -> *) vn.
(Functor f, Ord vn) =>
PatBase f vn -> Set vn
patNames Pat
forpat
            While {} -> forall a. Monoid a => a
mempty
        loopt' :: PatType
loopt' =
          forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map VName -> Alias
AliasBound Names
bound_here) forall a b. (a -> b) -> a -> b
$
            PatType
loopt forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
Unique

    forall (f :: * -> *) a. Applicative f => a -> f a
pure (([VName]
sparams, Pat
mergepat'', Exp
mergeexp', LoopFormBase Info VName
form', Exp
loopbody'), PatType -> [VName] -> AppRes
AppRes PatType
loopt' [VName]
retext)