Improve core linter so it catches unsafeCoerce problems (T9122)

Summary:
This is a draft of the patch that is sent for review.

In this patch required changes in linter were introduced
and actual check:

 - new helper function: primRepSizeB
 - primRep check for floating
 - Add access to dynamic flags in linter.
 - Implement additional lint rules.

Reviewers: austin, goldfire, simonpj

Reviewed By: simonpj

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D637

GHC Trac Issues: #9122

8 files changed, 113 insertions, 21 deletions

diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 5ae7a59459..5338359f02 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -89,6 +89,7 @@ We check for
         (b) Out-of-scope type variables
         (c) Out-of-scope local variables
         (d) Ill-kinded types
+        (e) Incorrect unsafe coercions
 
 If we have done specialisation the we check that there are
         (a) No top-level bindings of primitive (unboxed type)
@@ -122,6 +123,25 @@ For Ids, the type-substituted Id is added to the in_scope set (which
 itself is part of the TvSubst we are carrying down), and when we
 find an occurrence of an Id, we fetch it from the in-scope set.
 
+Note [Bad unsafe coercion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+For discussion see https://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions
+Linter introduces additional rules that checks improper coercion between
+different types, called bad coercions. Following coercions are forbidden:
+
+  (a) coercions between boxed and unboxed values;
+  (b) coercions between unlifted values of the different sizes, here
+      active size is checked, i.e. size of the actual value but not
+      the space allocated for value;
+  (c) coercions between floating and integral boxed values, this check
+      is not yet supported for unboxed tuples, as no semantics were
+      specified for that;
+  (d) coercions from / to vector type
+  (e) If types are unboxed tuples then tuple (# A_1,..,A_n #) can be
+      coerced to (# B_1,..,B_m #) if n=m and for each pair A_i, B_i rules
+      (a-e) holds.
+
 ************************************************************************
 *                                                                      *
                  Beginning and ending passes
@@ -230,7 +250,7 @@ lintPassResult hsc_env pass binds
   | not (gopt Opt_DoCoreLinting dflags)
   = return ()
   | otherwise
-  = do { let (warns, errs) = lintCoreBindings pass (interactiveInScope hsc_env) binds
+  = do { let (warns, errs) = lintCoreBindings dflags pass (interactiveInScope hsc_env) binds
        ; Err.showPass dflags ("Core Linted result of " ++ showPpr dflags pass)
        ; displayLintResults dflags pass warns errs binds  }
   where
@@ -272,7 +292,7 @@ lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO ()
 lintInteractiveExpr what hsc_env expr
   | not (gopt Opt_DoCoreLinting dflags)
   = return ()
-  | Just err <- lintExpr (interactiveInScope hsc_env) expr
+  | Just err <- lintExpr dflags (interactiveInScope hsc_env) expr
   = do { display_lint_err err
        ; Err.ghcExit dflags 1 }
   | otherwise
@@ -316,12 +336,12 @@ interactiveInScope hsc_env
               --   f :: [t] -> [t]
               -- where t is a RuntimeUnk (see TcType)
 
-lintCoreBindings :: CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
+lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
 --   Returns (warnings, errors)
 -- If you edit this function, you may need to update the GHC formalism
 -- See Note [GHC Formalism]
-lintCoreBindings pass local_in_scope binds
-  = initL flags $
+lintCoreBindings dflags pass local_in_scope binds
+  = initL dflags flags $
     addLoc TopLevelBindings        $
     addInScopeVars local_in_scope  $
     addInScopeVars binders         $
@@ -378,29 +398,31 @@ We use this to check all unfoldings that come in from interfaces
 (it is very painful to catch errors otherwise):
 -}
 
-lintUnfolding :: SrcLoc
+lintUnfolding :: DynFlags
+              -> SrcLoc
               -> [Var]          -- Treat these as in scope
               -> CoreExpr
               -> Maybe MsgDoc   -- Nothing => OK
 
-lintUnfolding locn vars expr
+lintUnfolding dflags locn vars expr
   | isEmptyBag errs = Nothing
   | otherwise       = Just (pprMessageBag errs)
   where
-    (_warns, errs) = initL defaultLintFlags linter
+    (_warns, errs) = initL dflags defaultLintFlags linter
     linter = addLoc (ImportedUnfolding locn) $
              addInScopeVars vars             $
              lintCoreExpr expr
 
-lintExpr :: [Var]               -- Treat these as in scope
+lintExpr :: DynFlags
+         -> [Var]               -- Treat these as in scope
          -> CoreExpr
          -> Maybe MsgDoc        -- Nothing => OK
 
-lintExpr vars expr
+lintExpr dflags vars expr
   | isEmptyBag errs = Nothing
   | otherwise       = Just (pprMessageBag errs)
   where
-    (_warns, errs) = initL defaultLintFlags linter
+    (_warns, errs) = initL dflags defaultLintFlags linter
     linter = addLoc TopLevelBindings $
              addInScopeVars vars     $
              lintCoreExpr expr
@@ -1124,13 +1146,48 @@ lintCoercion (CoVarCo cv)
                                      2 (ppr cv)) }
        ; return (k, s, t, r) }
 
+-- See Note [Bad unsafe coercion]
 lintCoercion (UnivCo _prov r ty1 ty2)
   = do { k1 <- lintType ty1
-       ; _k2 <- lintType ty2
+       ; k2 <- lintType ty2
 --       ; unless (k1 `eqKind` k2) $
 --         failWithL (hang (ptext (sLit "Unsafe coercion changes kind"))
 --                       2 (ppr co))
+       ; when (r /= Phantom && isSubOpenTypeKind k1 && isSubOpenTypeKind k2)
+              (checkTypes ty1 ty2)
        ; return (k1, ty1, ty2, r) }
+   where
+     report s = hang (text $ "Unsafe coercion between " ++ s)
+                     2 (vcat [ text "From:" <+> ppr ty1
+                             , text "  To:" <+> ppr ty2])
+     isUnBoxed :: PrimRep -> Bool
+     isUnBoxed PtrRep = False
+     isUnBoxed _      = True
+     checkTypes t1 t2
+       = case (repType t1, repType t2) of
+           (UnaryRep _, UnaryRep _) ->
+              validateCoercion (typePrimRep t1)
+                               (typePrimRep t2)
+           (UbxTupleRep rep1, UbxTupleRep rep2) -> do
+              checkWarnL (length rep1 == length rep2)
+                         (report "unboxed tuples of different length")
+              zipWithM_ checkTypes rep1 rep2
+           _  -> addWarnL (report "unboxed tuple and ordinary type")
+     validateCoercion :: PrimRep -> PrimRep -> LintM ()
+     validateCoercion rep1 rep2
+       = do { dflags <- getDynFlags
+            ; checkWarnL (isUnBoxed rep1 == isUnBoxed rep2)
+                         (report "unboxed and boxed value")
+            ; checkWarnL (TyCon.primRepSizeW dflags rep1
+                           == TyCon.primRepSizeW dflags rep2)
+                         (report "unboxed values of different size")
+            ; let fl = liftM2 (==) (TyCon.primRepIsFloat rep1)
+                                   (TyCon.primRepIsFloat rep2)
+            ; case fl of
+                Nothing    -> addWarnL (report "vector types")
+                Just False -> addWarnL (report "float and integral values")
+                _          -> return ()
+            }
 
 lintCoercion (SymCo co)
   = do { (k, ty1, ty2, r) <- lintCoercion co
@@ -1288,8 +1345,10 @@ data LintEnv
   = LE { le_flags :: LintFlags       -- Linting the result of this pass
        , le_loc   :: [LintLocInfo]   -- Locations
        , le_subst :: TvSubst         -- Current type substitution; we also use this
-    }                                -- to keep track of all the variables in scope,
+                                     -- to keep track of all the variables in scope,
                                      -- both Ids and TyVars
+       , le_dynflags :: DynFlags     -- DynamicFlags
+       }
 
 data LintFlags
   = LF { lf_check_global_ids           :: Bool -- See Note [Checking for global Ids]
@@ -1344,6 +1403,9 @@ instance Monad LintM where
                            Just r -> unLintM (k r) env errs'
                            Nothing -> (Nothing, errs'))
 
+instance HasDynFlags LintM where
+  getDynFlags = LintM (\ e errs -> (Just (le_dynflags e), errs))
+
 data LintLocInfo
   = RhsOf Id            -- The variable bound
   | LambdaBodyOf Id     -- The lambda-binder
@@ -1356,12 +1418,12 @@ data LintLocInfo
   | InType Type         -- Inside a type
   | InCo   Coercion     -- Inside a coercion
 
-initL :: LintFlags -> LintM a -> WarnsAndErrs    -- Errors and warnings
-initL flags m
+initL :: DynFlags -> LintFlags -> LintM a -> WarnsAndErrs    -- Errors and warnings
+initL dflags flags m
   = case unLintM m env (emptyBag, emptyBag) of
       (_, errs) -> errs
   where
-    env = LE { le_flags = flags, le_subst = emptyTvSubst, le_loc = [] }
+    env = LE { le_flags = flags, le_subst = emptyTvSubst, le_loc = [], le_dynflags = dflags }
 
 getLintFlags :: LintM LintFlags
 getLintFlags = LintM $ \ env errs -> (Just (le_flags env), errs)
@@ -1370,6 +1432,10 @@ checkL :: Bool -> MsgDoc -> LintM ()
 checkL True  _   = return ()
 checkL False msg = failWithL msg
 
+checkWarnL :: Bool -> MsgDoc -> LintM ()
+checkWarnL True   _  = return ()
+checkWarnL False msg = addWarnL msg
+
 failWithL :: MsgDoc -> LintM a
 failWithL msg = LintM $ \ env (warns,errs) ->
                 (Nothing, (warns, addMsg env errs msg))
diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs
index d76ce8d7b2..40543b711c 100644
--- a/compiler/iface/TcIface.hs
+++ b/compiler/iface/TcIface.hs
@@ -1196,7 +1196,8 @@ tcPragExpr name expr
                 -- Check for type consistency in the unfolding
     whenGOptM Opt_DoCoreLinting $ do
         in_scope <- get_in_scope
-        case lintUnfolding noSrcLoc in_scope core_expr' of
+        dflags   <- getDynFlags
+        case lintUnfolding dflags noSrcLoc in_scope core_expr' of
           Nothing       -> return ()
           Just fail_msg -> do { mod <- getIfModule
                               ; pprPanic "Iface Lint failure"
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 514273cf64..8e0175a6cf 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -85,6 +85,7 @@ module TyCon(
         PrimRep(..), PrimElemRep(..),
         tyConPrimRep, isVoidRep, isGcPtrRep,
         primRepSizeW, primElemRepSizeB,
+        primRepIsFloat,
 
         -- * Recursion breaking
         RecTcChecker, initRecTc, checkRecTc
@@ -980,6 +981,14 @@ primElemRepSizeB Word64ElemRep = 8
 primElemRepSizeB FloatElemRep  = 4
 primElemRepSizeB DoubleElemRep = 8
 
+-- | Return if Rep stands for floating type,
+-- returns Nothing for vector types.
+primRepIsFloat :: PrimRep -> Maybe Bool
+primRepIsFloat  FloatRep     = Just True
+primRepIsFloat  DoubleRep    = Just True
+primRepIsFloat  (VecRep _ _) = Nothing
+primRepIsFloat  _            = Just False
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 56b4b99151..6015731257 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -207,9 +207,11 @@ k /= BOX
 ----------------------- :: CoVarCoRepr
 G |-co z_(s ~R#k t) : s ~Rep k t
 
-G |-ty t1 : k
------------------------------ :: UnivCo
-G |-co t1 ==>!_R t2 : t1 ~R k t2
+G |-ty t1 : k1
+G |-ty t2 : k2
+R <= Phant \/ not (k1 <: OpenKind) \/ not (k2 <: OpenKind) \/ compatibleUnBoxedTys t1 t2
+------------------------------------------------------------------------ :: UnivCo
+G |-co t1 ==>!_R t2 : t1 ~R k2 t2
 
 G |-co g : t1 ~R k t2
 ------------------------- :: SymCo
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index 0c5b30483e..d64667af18 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -278,6 +278,7 @@ terminals :: 'terminals_' ::=
   | vars_of      ::   :: vars_of          {{ tex \textsf{vars\_of } }}
   | not          ::   :: not              {{ tex \neg }}
   | isUnLiftedTyCon :: :: isUnLiftenTyCon {{ tex \textsf{isUnLiftedTyCon} }}
+  | compatibleUnBoxedTys :: :: compatibleUnBoxedTys {{ tex \textsf{compatibleUnBoxedTys} }}
   | false        ::   :: false            {{ tex \textsf{false} }}
   | true         ::   :: true             {{ tex \textsf{true} }}
   | \/           ::   :: or               {{ tex \vee }}
@@ -333,6 +334,7 @@ formula :: 'formula_' ::=
   | no_duplicates </ bindingi // i />  ::   :: no_duplicates_binding
   | not formula                        ::   :: not
   | isUnLiftedTyCon T                  ::   :: isUnLiftedTyCon
+  | compatibleUnBoxedTys t1 t2         ::   :: compatibleUnBoxedTys
   | formula1 /\ formula2               ::   :: and
   | formula1 \/ formula2               ::   :: or
   | ( formula )                        ::   :: parens
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 28540ac8e9..ddbc6147d4 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -196,6 +196,18 @@ a list of coercions. This is elided in this presentation, as we simply identify
 axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.lhs}{mkBinAxiom}
 and \coderef{typecheck/TcTypeNats.lhs}{mkAxiom1}.
 
+In \ottdrulename{Co\_UnivCo}, function $ \textsf{compatibleUnBoxedTys} $ stands for following checks:
+\begin{itemize}
+    \item both types are unboxed;
+    \item types should have same size;
+    \item both types should be either integral or floating;
+    \item coercion between vector types are not allowed;
+    \item unboxed tuples should have same length and each element should be coercible to
+    appropriate element of the target tuple;
+\end{itemize}
+For function implementation see \coderef{coreSyn/CoreLint.lhs}{checkTypes}.
+For futher discussion see \url{https://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions}.
+
 \subsection{Type constructors}
 
 Type constructors in GHC contain \emph{lots} of information. We leave most of it out
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 52f2e39f83..8d2e5cbb13 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf
diff --git a/testsuite/tests/callarity/unittest/CallArity1.hs b/testsuite/tests/callarity/unittest/CallArity1.hs
index dbcac513a1..a92a73b4f2 100644
--- a/testsuite/tests/callarity/unittest/CallArity1.hs
+++ b/testsuite/tests/callarity/unittest/CallArity1.hs
@@ -162,7 +162,7 @@ main = do
         getSessionDynFlags >>= setSessionDynFlags . flip gopt_set Opt_SuppressUniques
         dflags <- getSessionDynFlags
         liftIO $ forM_ exprs $ \(n,e) -> do
-            case lintExpr [f,scrut] e of
+            case lintExpr dflags [f,scrut] e of
                 Just msg -> putMsg dflags (msg $$ text "in" <+> text n)
                 Nothing -> return ()
             putMsg dflags (text n <> char ':')