Commit d09e982c authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent 7301404d
......@@ -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
......
{-# 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)
==================== Tidy Core rules ====================
"SPEC shared @ []" [ALWAYS]
forall ($dMyFunctor :: MyFunctor []) (irred :: Domain [] Int).
forall (irred :: Domain [] Int) ($dMyFunctor :: MyFunctor []).
shared @ [] $dMyFunctor irred
= bar_$sshared
......
......@@ -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'])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment