Fix #450, check conjunctiveness when splitting

Before this commit, there was a bug when checking of whether an unpack was
allowed that lead to code like `let read Get, linear Set = consume Cell`
compiling. This is now fixed so that all types in an unpack needs to be
separated by a conjunction in the capability being unpacked, unless all
the types can safely be (at least locally) aliased.

A known bug is that we also need to check that the modes are preserved
for all types in an upcast, meaning that the `read Get` above should
also be `linear` (assuming `Get` and `Set` are conjunctive in `Cell`).

src/types/Typechecker/Typechecker.hs

@@ -616,9 +616,9 @@ instance Checkable Expr where
                          Var{varName} -> (varName, eType)}
                 localBindings = map extractBindings eVars
                 varTypes = map snd localBindings
-            linearTypes <- filterM isLinearType varTypes
-            when (length linearTypes > 1) $
-                 checkConjunction eType linearTypes
+            allAliasable <- allM isAliasableType varTypes
+            unless (allAliasable || length varTypes == 1) $
+                 checkConjunction eType varTypes
             (locals, eDecls) <-
                 local (extendEnvironment localBindings) $
                       typecheckDecls decls'

src/types/Typechecker/Util.hs

@@ -6,6 +6,7 @@ module Typechecker.Util(TypecheckM
                        ,CapturecheckM
                        ,whenM
                        ,anyM
+                       ,allM
                        ,unlessM
                        ,tcError
                        ,tcWarning
@@ -24,6 +25,7 @@ module Typechecker.Util(TypecheckM
                        ,isSubordinateType
                        ,isEncapsulatedType
                        ,isThreadType
+                       ,isAliasableType
                        ,checkConjunction
                        ) where
 
@@ -424,6 +426,23 @@ isThreadType ty
         anyM isThreadType (getArgTypes ty)
     | otherwise = return $ isThreadRefType ty
 
+isUnsafeType :: Type -> TypecheckM Bool
+isUnsafeType ty
+    | isPassiveClassType ty = do
+        capability <- findCapability ty
+        isUnsafeType capability
+    | otherwise = return $
+                  any isUnsafeRefType $ typeComponents ty
+
+isAliasableType :: Type -> TypecheckM Bool
+isAliasableType ty =
+    anyM (\f -> f ty)
+         [return . isSafeType
+         ,isThreadType
+         ,isSubordinateType
+         ,isUnsafeType
+         ]
+
 checkConjunction :: Type -> [Type] -> TypecheckM ()
 checkConjunction source sinks
   | isCompositeType source = do
@@ -432,6 +451,12 @@ checkConjunction source sinks
                                           (sinks \\ [ty]) ty) sinks
   | isPassiveClassType source = do
       cap <- findCapability source
+      when (isIncapability cap) $
+           tcError $ "Cannot unpack empty capability of class '" ++
+                     show source ++ "'"
+      when (source `elem` sinks) $
+           tcError $ "Unpacking of " ++ Ty.showWithKind cap ++
+                     " cannot be inferred. Try adding type annotations"
       checkConjunction cap sinks
   | otherwise =
       return ()

src/types/Types.hs

@@ -97,6 +97,7 @@ module Types(
             ,isThreadRefType
             ,isReadRefType
             ,isSubordinateRefType
+            ,isUnsafeRefType
             ,makeStackbound
             ,isStackboundType
             ) where
@@ -619,6 +620,10 @@ isSubordinateRefType ty
     | Just Subordinate <- getMode ty = True
     | otherwise = False
 
+isUnsafeRefType ty
+    | Just Unsafe <- getMode ty = True
+    | otherwise = False
+
 isCapabilityType Type{inner = CapabilityType{}} = True
 isCapabilityType Type{inner = TraitType{}} = True
 isCapabilityType Type{inner = EmptyCapability{}} = True