[commit: ghc] master: Do not bind coercion variables in SpecConstr rules (fb050a3)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/fb050a330ad202c1eb43038dc18cca2a5be26f4a/ghc

>---------------------------------------------------------------

commit fb050a330ad202c1eb43038dc18cca2a5be26f4a
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Thu Oct 12 11:00:19 2017 +0100

    Do not bind coercion variables in SpecConstr rules
    
    Trac #14270 showed that SpecConstr could cause nasty Lint failures
    if it generates a RULE that binds coercion varables.  See
    
     * Note [SpecConstr and casts], and
     * the test simplCore/should_compile/T14270.
    
    This doesn't feel like the final word to me, because somehow the
    specialisation "ought" to work.  So I left in a debug WARN to yell if
    the new check acutally fires.
    
    Meanwhile, it stops the erroneous specialisation.
    
    binding coercion


>---------------------------------------------------------------

fb050a330ad202c1eb43038dc18cca2a5be26f4a
 compiler/specialise/SpecConstr.hs                  | 44 +++++++++++++++++++++-
 .../tests/simplCore/should_compile/T14270a.hs      | 27 +++++++++++++
 testsuite/tests/simplCore/should_compile/all.T     |  1 +
 3 files changed, 70 insertions(+), 2 deletions(-)

diff --git a/compiler/specialise/SpecConstr.hs b/compiler/specialise/SpecConstr.hs
index 609e70c..86d7093 100644
--- a/compiler/specialise/SpecConstr.hs
+++ b/compiler/specialise/SpecConstr.hs
@@ -1883,6 +1883,41 @@ by trim_pats.
 
 * Otherwise we sort the patterns to choose the most general
   ones first; more general => more widely applicable.
+
+Note [SpecConstr and casts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (Trac #14270) a call like
+
+    let f = e
+    in ... f (K @(a |> co)) ...
+
+where 'co' is a coercion variable not in scope at f's definition site.
+If we aren't caereful we'll get
+
+    let $sf a co = e (K @(a |> co))
+        RULE "SC:f" forall a co.  f (K @(a |> co)) = $sf a co
+        f = e
+    in ...
+
+But alas, when we match the call we won't bind 'co', because type-matching
+(for good reasons) discards casts).
+
+I don't know how to solve this, so for now I'm just discarding any
+call patterns that
+  * Mentions a coercion variable
+  * That is not in scope at the binding of the function
+
+I think this is very rare.
+
+Note that this /also/ discards the call pattern if we have a cast in a
+/term/, although in fact Rules.match does make a very flaky and
+fragile attempt to match coercions.  e.g. a call like
+    f (Maybe Age) (Nothing |> co) blah
+    where co :: Maybe Int ~ Maybe Age
+will be discarded.  It's extremely fragile to match on the form of a
+coercion, so I think it's better just not to try.  A more complicated
+alternative would be to discard calls that mention coercion variables
+only in kind-casts, but I'm doing the simple thing for now.
 -}
 
 type CallPat = ([Var], [CoreExpr])      -- Quantified variables and arguments
@@ -1985,7 +2020,7 @@ callToPats :: ScEnv -> [ArgOcc] -> Call -> UniqSM (Maybe CallPat)
         --      Type variables come first, since they may scope
         --      over the following term variables
         -- The [CoreExpr] are the argument patterns for the rule
-callToPats env bndr_occs (Call _ args con_env)
+callToPats env bndr_occs call@(Call _ args con_env)
   | args `ltLength` bndr_occs      -- Check saturated
   = return Nothing
   | otherwise
@@ -2014,8 +2049,13 @@ callToPats env bndr_occs (Call _ args con_env)
               sanitise id   = id `setIdType` expandTypeSynonyms (idType id)
                 -- See Note [Free type variables of the qvar types]
 
+              bad_covars = filter isCoVar ids
+                -- See Note [SpecConstr and casts]
+
         ; -- pprTrace "callToPats"  (ppr args $$ ppr bndr_occs) $
-          if interesting
+          WARN( not (null bad_covars), text "SpecConstr: bad covars:" <+> ppr bad_covars
+                                       $$ ppr call )
+          if interesting && null bad_covars
           then return (Just (qvars', pats))
           else return Nothing }
 
diff --git a/testsuite/tests/simplCore/should_compile/T14270a.hs b/testsuite/tests/simplCore/should_compile/T14270a.hs
new file mode 100644
index 0000000..840b1e8
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T14270a.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE TypeApplications, ScopedTypeVariables, GADTs, RankNTypes, TypeInType, KindSignatures #-}
+{-# OPTIONS_GHC -O2 #-} -- We are provoking a bug in SpecConstr
+
+module T14270a where
+
+import Data.Kind
+import Data.Proxy
+
+data T a = T1 (T a) | T2
+
+data K (a :: k) where
+  K1 :: K (a :: Type)
+  K2 :: K a
+
+f :: T (a :: Type) -> Bool
+f (T1 x) = f x
+f T2     = True
+
+g :: forall (a :: k). K a -> T a -> Bool
+g kv x = case kv of
+            K1 -> f @a T2   -- f @a (T1 x) gives a different crash
+            k2 -> True
+
+-- The point here is that the call to f looks like
+--    f @(a |> co) (T2 @(a |> co))
+-- where 'co' is bound by the pattern match on K1
+-- See Note [SpecConstr and casts] in SpecConstr
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 7f21331..28e26ed 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -281,3 +281,4 @@ test('T14140',
      ['$MAKE -s --no-print-directory T14140'])
 
 test('T14272', normal, compile, [''])
+test('T14270a', normal, compile, [''])