[commit: ghc] master: Don't quantify over Refl in a RULE (d09e982)
git at git.haskell.org
git at git.haskell.org
Tue Jun 21 13:49:09 UTC 2016
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/d09e982c534b20908064f36d701a1a3a6a2eb55a/ghc
>---------------------------------------------------------------
commit d09e982c534b20908064f36d701a1a3a6a2eb55a
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.
>---------------------------------------------------------------
d09e982c534b20908064f36d701a1a3a6a2eb55a
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 d587eeb..abd15c8 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 )
@@ -1227,6 +1227,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
@@ -1249,9 +1252,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
@@ -1335,7 +1339,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 ddac42c..ecf990c 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -240,3 +240,4 @@ test('T3990',
test('T12076', extra_clean(['T12076a.hi', 'T12076a.o']), multimod_compile, ['T12076', '-v0'])
test('T12076lit', normal, compile, ['-O'])
test('T12076sat', normal, compile, ['-O'])
+test('T12212', normal, compile, ['-O'])
More information about the ghc-commits
mailing list