Type-check aliasing in separate pass (diku-dk#1977)

This significantly simplifies the type checker, and also fixes known
(and future) bugs related to tracking aliases of an incompletely typed
term.

This also allows us to provide better error messages, although it's
possible that they are currently slightly worse, as the aliasing
checking does not use the "context" mechanism of the term-level type
checker.

The AST itself is simplified because it no longer has to embed alias
information (which wasn't correct anyway, and was not actually used).

There is one user-visible change: lambdas that must return an
alias-free result will now require a return type annotation. We may
loosen this in the future, but it is a very rare case in practice.

Closes diku-dk#1872.

CHANGELOG.md

@@ -25,6 +25,12 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
   multidimensional variants), as well as `split`, now have more
   precise types.
 
+* Local and anonymous (lambda) functions that *must* return unique
+  results (because they are passed to a higher order function that
+  requires this) must now have an explicit return type ascription that
+  declares this, using `*`.  This is very rare (in practice
+  unobserved) in real programs.
+
 ### Fixed
 
 * `futhark doc` produced some invalid links.

futhark.cabal

@@ -443,6 +443,7 @@ library
       Language.Futhark.Traversals
       Language.Futhark.Tuple
       Language.Futhark.TypeChecker
+      Language.Futhark.TypeChecker.Consumption
       Language.Futhark.TypeChecker.Match
       Language.Futhark.TypeChecker.Modules
       Language.Futhark.TypeChecker.Monad

src/Futhark/Doc/Generator.hs

@@ -6,6 +6,7 @@ import Control.Arrow ((***))
 import Control.Monad
 import Control.Monad.Reader
 import Control.Monad.Writer (Writer, WriterT, runWriter, runWriterT, tell)
+import Data.Bifunctor (second)
 import Data.Char (isAlpha, isSpace, toUpper)
 import Data.List (find, groupBy, inits, intersperse, isPrefixOf, partition, sort, sortOn, tails)
 import Data.Map qualified as M
@@ -417,9 +418,7 @@ valBindHtml :: Html -> ValBind -> DocM (Html, Html, Html)
 valBindHtml name (ValBind _ _ retdecl (Info rettype) tparams params _ _ _ _) = do
   let tparams' = mconcat $ map ((" " <>) . typeParamHtml) tparams
       noLink' =
-        noLink $
-          map typeParamName tparams
-            ++ map identName (S.toList $ mconcat $ map patIdents params)
+        noLink $ map typeParamName tparams ++ S.toList (foldMap patNames params)
   rettype' <- noLink' $ maybe (retTypeHtml rettype) typeExpHtml retdecl
   params' <- noLink' $ mapM paramHtml params
   pure
@@ -481,13 +480,13 @@ renderValBind = fmap H.div . synopsisValBindBind
 
 renderTypeBind :: (VName, TypeBinding) -> DocM Html
 renderTypeBind (name, TypeAbbr l tps tp) = do
-  tp' <- retTypeHtml tp
+  tp' <- retTypeHtml $ toResRet Nonunique tp
   pure $ H.div $ typeAbbrevHtml l (vnameHtml name) tps <> " = " <> tp'
 
 synopsisValBindBind :: (VName, BoundV) -> DocM Html
 synopsisValBindBind (name, BoundV tps t) = do
   let tps' = map typeParamHtml tps
-  t' <- typeHtml t
+  t' <- typeHtml $ second (const Nonunique) t
   pure $
     keyword "val "
       <> vnameHtml name
@@ -499,11 +498,11 @@ dietHtml :: Diet -> Html
 dietHtml Consume = "*"
 dietHtml Observe = ""
 
-typeHtml :: StructType -> DocM Html
+typeHtml :: TypeBase Size Uniqueness -> DocM Html
 typeHtml t = case t of
-  Array _ u shape et -> do
+  Array u shape et -> do
     shape' <- prettyShape shape
-    et' <- typeHtml $ Scalar et
+    et' <- typeHtml $ Scalar $ second (const Nonunique) et
     pure $ prettyU u <> shape' <> et'
   Scalar (Prim et) -> pure $ primTypeHtml et
   Scalar (Record fs)
@@ -515,12 +514,12 @@ typeHtml t = case t of
       ppField (name, tp) = do
         tp' <- typeHtml tp
         pure $ toHtml (nameToString name) <> ": " <> tp'
-  Scalar (TypeVar _ u et targs) -> do
+  Scalar (TypeVar u et targs) -> do
     targs' <- mapM typeArgHtml targs
     et' <- qualNameHtml et
     pure $ prettyU u <> et' <> mconcat (map (" " <>) targs')
   Scalar (Arrow _ pname d t1 t2) -> do
-    t1' <- typeHtml t1
+    t1' <- typeHtml $ second (const Nonunique) t1
     t2' <- retTypeHtml t2
     pure $ case pname of
       Named v ->
@@ -532,7 +531,7 @@ typeHtml t = case t of
       ppClause (n, ts) = joinBy " " . (ppConstr n :) <$> mapM typeHtml ts
       ppConstr name = "#" <> toHtml (nameToString name)
 
-retTypeHtml :: StructRetType -> DocM Html
+retTypeHtml :: ResRetType -> DocM Html
 retTypeHtml (RetType [] t) = typeHtml t
 retTypeHtml (RetType dims t) = do
   t' <- typeHtml t
@@ -544,7 +543,7 @@ prettyShape (Shape ds) =
 
 typeArgHtml :: TypeArg Size -> DocM Html
 typeArgHtml (TypeArgDim d) = dimDeclHtml d
-typeArgHtml (TypeArgType t) = typeHtml t
+typeArgHtml (TypeArgType t) = typeHtml $ second (const Nonunique) t
 
 modParamHtml :: [ModParamBase Info VName] -> DocM Html
 modParamHtml [] = pure mempty
@@ -695,10 +694,10 @@ vnameLink' (VName _ tag) current file =
     then "#" ++ show tag
     else relativise file current -<.> ".html#" ++ show tag
 
-paramHtml :: Pat -> DocM Html
+paramHtml :: Pat ParamType -> DocM Html
 paramHtml pat = do
   let (pat_param, d, t) = patternParam pat
-  t' <- typeHtml t
+  t' <- typeHtml $ second (const Nonunique) t
   pure $ case pat_param of
     Named v -> parens (vnameHtml v <> ": " <> dietHtml d <> t')
     Unnamed -> t'

src/Futhark/IR/Pretty.hs

@@ -43,9 +43,6 @@ instance Pretty Commutativity where
   pretty Commutative = "commutative"
   pretty Noncommutative = "noncommutative"
 
-instance Pretty NoUniqueness where
-  pretty _ = mempty
-
 instance Pretty Shape where
   pretty = mconcat . map (brackets . pretty) . shapeDims
 

src/Futhark/IR/Syntax/Core.hs

@@ -12,7 +12,6 @@ module Futhark.IR.Syntax.Core
     -- * Types
     Commutativity (..),
     Uniqueness (..),
-    NoUniqueness (..),
     ShapeBase (..),
     Shape,
     stripDims,
@@ -221,16 +220,6 @@ data Space
 -- | A string representing a specific non-default memory space.
 type SpaceId = String
 
--- | A fancier name for @()@ - encodes no uniqueness information.
-data NoUniqueness = NoUniqueness
-  deriving (Eq, Ord, Show)
-
-instance Semigroup NoUniqueness where
-  NoUniqueness <> NoUniqueness = NoUniqueness
-
-instance Monoid NoUniqueness where
-  mempty = NoUniqueness
-
 -- | The type of a value.  When comparing types for equality with
 -- '==', shapes must match.
 data TypeBase shape u

src/Futhark/Internalise/Bindings.hs

@@ -42,15 +42,15 @@ treeLike (Free ls) bs = Free $ zipWith treeLike ls (chunks (map length ls) bs)
 
 bindingFParams ::
   [E.TypeParam] ->
-  [E.Pat] ->
+  [E.Pat E.ParamType] ->
   ([I.FParam I.SOACS] -> [[Tree (I.FParam I.SOACS)]] -> InternaliseM a) ->
   InternaliseM a
 bindingFParams tparams params m = do
   flattened_params <- mapM flattenPat params
   let params_idents = concat flattened_params
   params_ts <-
     internaliseParamTypes $
-      map (flip E.setAliases () . E.unInfo . E.identType . fst) params_idents
+      map (E.unInfo . E.identType . fst) params_idents
   let num_param_idents = map length flattened_params
 
   let shape_params = [I.Param mempty v $ I.Prim I.int64 | E.TypeParamDim v _ <- tparams]
@@ -86,13 +86,13 @@ bindingFParams tparams params m = do
 
 bindingLoopParams ::
   [E.TypeParam] ->
-  E.Pat ->
+  E.Pat E.ParamType ->
   [I.Type] ->
   ([I.FParam I.SOACS] -> [I.FParam I.SOACS] -> InternaliseM a) ->
   InternaliseM a
 bindingLoopParams tparams pat ts m = do
   pat_idents <- flattenPat pat
-  pat_ts <- internaliseLoopParamType (E.patternStructType pat) ts
+  pat_ts <- internaliseLoopParamType (E.patternType pat) ts
 
   let shape_params = [I.Param mempty v $ I.Prim I.int64 | E.TypeParamDim v _ <- tparams]
       shape_subst = M.fromList [(I.paramName p, [I.Var $ I.paramName p]) | p <- shape_params]
@@ -103,7 +103,7 @@ bindingLoopParams tparams pat ts m = do
         m shape_params (concat valueparams)
 
 bindingLambdaParams ::
-  [E.Pat] ->
+  [E.Pat E.ParamType] ->
   [I.Type] ->
   ([I.LParam I.SOACS] -> InternaliseM a) ->
   InternaliseM a
@@ -118,7 +118,7 @@ type Params t = [I.Param t]
 
 processFlatPat ::
   Show t =>
-  [(E.Ident, [E.AttrInfo VName])] ->
+  [(E.Ident ParamType, [E.AttrInfo VName])] ->
   [t] ->
   InternaliseM ([Params t], VarSubsts)
 processFlatPat x y = processFlatPat' [] x y
@@ -142,7 +142,7 @@ processFlatPat x y = processFlatPat' [] x y
     handleMapping _ [] _ =
       error $ "handleMapping: insufficient identifiers in pattern.\n" ++ show (x, y)
 
-    internaliseBindee :: E.Ident -> InternaliseM [VName]
+    internaliseBindee :: E.Ident E.ParamType -> InternaliseM [VName]
     internaliseBindee bindee = do
       let name = E.identName bindee
       case internalisedTypeSize $ E.unInfo $ E.identType bindee of
@@ -151,7 +151,7 @@ processFlatPat x y = processFlatPat' [] x y
 
 bindingFlatPat ::
   Show t =>
-  [(E.Ident, [E.AttrInfo VName])] ->
+  [(E.Ident E.ParamType, [E.AttrInfo VName])] ->
   [t] ->
   ([Params t] -> InternaliseM a) ->
   InternaliseM a
@@ -161,7 +161,7 @@ bindingFlatPat idents ts m = do
     m ps
 
 -- | Flatten a pattern.  Returns a list of identifiers.
-flattenPat :: MonadFreshNames m => E.Pat -> m [(E.Ident, [E.AttrInfo VName])]
+flattenPat :: MonadFreshNames m => E.Pat (TypeBase Size u) -> m [(E.Ident (TypeBase Size u), [E.AttrInfo VName])]
 flattenPat = flattenPat'
   where
     flattenPat' (E.PatParens p _) =
@@ -189,7 +189,7 @@ flattenPat = flattenPat'
       concat <$> mapM flattenPat' ps
 
 stmPat ::
-  E.Pat ->
+  E.Pat E.ParamType ->
   [I.Type] ->
   ([VName] -> InternaliseM a) ->
   InternaliseM a