[commit: ghc] ghc-8.0: Don't quantify over Refl in a RULE (cd9c4a5)

git at git.haskell.org git at git.haskell.org
Mon Jul 25 18:36:38 UTC 2016


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

On branch  : ghc-8.0
Link       : http://ghc.haskell.org/trac/ghc/changeset/cd9c4a5db6500bb61bee2904a14d5969b1910b5a/ghc

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

commit cd9c4a5db6500bb61bee2904a14d5969b1910b5a
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Mon Jun 20 15:48:09 2016 +0100

    Don't quantify over Refl in a RULE
    
    This fixes Trac #12212.  It's quite hard to provoke, but I've
    added a standalone test case that does so.
    
    The issue is explained in Note [Evidence foralls] in Specialise.
    
    (cherry picked from commit d09e982c534b20908064f36d701a1a3a6a2eb55a)


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

cd9c4a5db6500bb61bee2904a14d5969b1910b5a
 compiler/specialise/Specialise.hs                  | 35 ++++++++++++++++++----
 testsuite/tests/simplCore/should_compile/T12212.hs | 17 +++++++++++
 .../tests/simplCore/should_compile/T7785.stderr    |  2 +-
 testsuite/tests/simplCore/should_compile/all.T     |  1 +
 4 files changed, 48 insertions(+), 7 deletions(-)

diff --git a/compiler/specialise/Specialise.hs b/compiler/specialise/Specialise.hs
index 0c1d398..33ce1ac 100644
--- a/compiler/specialise/Specialise.hs
+++ b/compiler/specialise/Specialise.hs
@@ -12,8 +12,8 @@ module Specialise ( specProgram, specUnfolding ) where
 import Id
 import TcType hiding( substTy )
 import Type   hiding( substTy, extendTvSubstList )
-import Coercion( Coercion )
 import Module( Module, HasModule(..) )
+import Coercion( Coercion )
 import CoreMonad
 import qualified CoreSubst
 import CoreUnfold
@@ -22,7 +22,7 @@ import VarEnv
 import CoreSyn
 import Rules
 import CoreUtils        ( exprIsTrivial, applyTypeToArgs, mkCast )
-import CoreFVs          ( exprFreeVars, exprsFreeVars, idFreeVars )
+import CoreFVs          ( exprFreeVars, exprsFreeVars, idFreeVars, exprsFreeIdsList )
 import UniqSupply
 import Name
 import MkId             ( voidArgId, voidPrimId )
@@ -1230,6 +1230,9 @@ specCalls mb_mod env rules_for_me calls_for_me fn rhs
 
         -- Construct the new binding
         --      f1 = SUBST[a->t1,c->t3, d1->d1', d2->d2'] (/\ b -> rhs)
+        -- PLUS the rule
+        --      RULE "SPEC f" forall b d1' d2'. f b d1' d2' = f1 b
+        --      In the rule, d1' and d2' are just wildcards, not used in the RHS
         -- PLUS the usage-details
         --      { d1' = dx1; d2' = dx2 }
         -- where d1', d2' are cloned versions of d1,d2, with the type substitution
@@ -1252,9 +1255,10 @@ specCalls mb_mod env rules_for_me calls_for_me fn rhs
            ; let (rhs_env2, dx_binds, spec_dict_args)
                             = bindAuxiliaryDicts rhs_env rhs_dict_ids call_ds inst_dict_ids
                  ty_args    = mk_ty_args call_ts poly_tyvars
-                 rule_args  = ty_args ++ map varToCoreExpr inst_dict_ids
-                                -- varToCoreExpr does the right thing for CoVars
-                 rule_bndrs = poly_tyvars ++ inst_dict_ids
+                 ev_args    = map varToCoreExpr inst_dict_ids  -- ev_args, ev_bndrs:
+                 ev_bndrs   = exprsFreeIdsList ev_args         -- See Note [Evidence foralls]
+                 rule_args  = ty_args     ++ ev_args
+                 rule_bndrs = poly_tyvars ++ ev_bndrs
 
            ; dflags <- getDynFlags
            ; if already_covered dflags rule_args then
@@ -1338,7 +1342,26 @@ specCalls mb_mod env rules_for_me calls_for_me fn rhs
 
            ; return (Just ((spec_f_w_arity, spec_rhs), final_uds, spec_env_rule)) } }
 
-{-
+{- Note [Evidence foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose (Trac #12212) that we are specialising
+   f :: forall a b. (Num a, F a ~ F b) => blah
+with a=b=Int. Then the RULE will be something like
+   RULE forall (d:Num Int) (g :: F Int ~ F Int).
+        f Int Int d g = f_spec
+But both varToCoreExpr (when constructing the LHS args), and the
+simplifier (when simplifying the LHS args), will transform to
+   RULE forall (d:Num Int) (g :: F Int ~ F Int).
+        f Int Int d <F Int> = f_spec
+by replacing g with Refl.  So now 'g' is unbound, which results in a later
+crash. So we use Refl right off the bat, and do not forall-quantify 'g':
+ * varToCoreExpr generates a Refl
+ * exprsFreeIdsList returns the Ids bound by the args,
+   which won't include g
+
+You might wonder if this will match as often, but the simplifer replaces
+complicated Refl coercions with Refl pretty aggressively.
+
 Note [Orphans and auto-generated rules]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we specialise an INLINEABLE function, or when we have
diff --git a/testsuite/tests/simplCore/should_compile/T12212.hs b/testsuite/tests/simplCore/should_compile/T12212.hs
new file mode 100644
index 0000000..ed284c3
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T12212.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T12212 where
+
+type family F a
+type instance F Int = Int
+
+foo :: a -> F a
+{-# NOINLINE foo #-}
+foo = undefined
+
+-- Inferred type
+-- forall a b. (Num a, F a ~# F b) => a -> b -> [F a]
+f x y = [ foo x, foo y ] ++ f (x-1) y
+
+-- Specialised call to f @ Int @ Int dNumInt <F Int ~ F Int>
+g = f (3::Int) (4::Int)
diff --git a/testsuite/tests/simplCore/should_compile/T7785.stderr b/testsuite/tests/simplCore/should_compile/T7785.stderr
index db80b99..c71a077 100644
--- a/testsuite/tests/simplCore/should_compile/T7785.stderr
+++ b/testsuite/tests/simplCore/should_compile/T7785.stderr
@@ -1,7 +1,7 @@
 
 ==================== Tidy Core rules ====================
 "SPEC shared @ []" [ALWAYS]
-    forall ($dMyFunctor :: MyFunctor []) (irred :: Domain [] Int).
+    forall (irred :: Domain [] Int) ($dMyFunctor :: MyFunctor []).
       shared @ [] $dMyFunctor irred
       = bar_$sshared
 
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index f50fd83..36b94c7 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -232,3 +232,4 @@ test('T11232', normal, compile, ['-O2'])
 test('T11562', normal, compile, ['-O2'])
 test('T11644', normal, compile, ['-O2'])
 test('T11742', normal, compile, ['-O2'])
+test('T12212', normal, compile, ['-O'])



More information about the ghc-commits mailing list