[commit: ghc] master: Make dischargeFmv handle Deriveds (57858fc)
git at git.haskell.org
git at git.haskell.org
Mon May 21 12:04:25 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/57858fc8b519078ae89a4859ce7588adb39f6e96/ghc
>---------------------------------------------------------------
commit 57858fc8b519078ae89a4859ce7588adb39f6e96
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Mon May 21 10:38:03 2018 +0100
Make dischargeFmv handle Deriveds
A Derived CFunEqCan does not "own" its FlatMetaTv (fmv), and should not
update it. But one caller (canCFunEqCan) was failing to satisfy the
precondition to dischargeFmv, which led to a crash (Trac #15170).
I fixed this by making dischargeFmv handle Deriveds (to avoid forcing
each caller to do so separately).
NB: this does not completely fix the original #15170 bug, but I'll
explain that on the ticket. The test case for this patch is actually
the program in comment:1.
>---------------------------------------------------------------
57858fc8b519078ae89a4859ce7588adb39f6e96
compiler/typecheck/TcFlatten.hs | 10 ++++++----
compiler/typecheck/TcInteract.hs | 10 ++--------
compiler/typecheck/TcRnTypes.hs | 4 ++--
compiler/typecheck/TcSMonad.hs | 19 +++++++++++++++----
testsuite/tests/polykinds/T15170.hs | 26 ++++++++++++++++++++++++++
testsuite/tests/polykinds/all.T | 1 +
6 files changed, 52 insertions(+), 18 deletions(-)
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index e2244a9..32a9307 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -82,15 +82,17 @@ Note [The flattening story]
- We unflatten Wanteds at the end of each attempt to simplify the
wanteds; see unflattenWanteds, called from solveSimpleWanteds.
-* Each canonical [G], [W], or [WD] CFunEqCan x : F xis ~ fsk/fmv
- has its own distinct evidence variable x and flatten-skolem fsk/fmv.
+* Ownership of fsk/fmv. Each canonical [G], [W], or [WD]
+ CFunEqCan x : F xis ~ fsk/fmv
+ "owns" a distinct evidence variable x, and flatten-skolem fsk/fmv.
Why? We make a fresh fsk/fmv when the constraint is born;
and we never rewrite the RHS of a CFunEqCan.
- In contrast a [D] CFunEqCan shares its fmv with its partner [W],
+ In contrast a [D] CFunEqCan /shares/ its fmv with its partner [W],
but does not "own" it. If we reduce a [D] F Int ~ fmv, where
say type instance F Int = ty, then we don't discharge fmv := ty.
- Rather we simply generate [D] fmv ~ ty (in TcInteract.reduce_top_fun_eq)
+ Rather we simply generate [D] fmv ~ ty (in TcInteract.reduce_top_fun_eq,
+ and dischargeFmv)
* Inert set invariant: if F xis1 ~ fsk1, F xis2 ~ fsk2
then xis1 /= xis2
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index ab94ad2..09cfd15 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -1442,15 +1442,9 @@ reactFunEq from_this fsk1 solve_this fsk2
; new_ev <- newGivenEvVar loc (fsk_eq_pred, evCoercion fsk_eq_co)
; emitWorkNC [new_ev] }
- | CtDerived { ctev_loc = loc } <- solve_this
- = do { traceTcS "reactFunEq (Derived)" (ppr from_this $$ ppr fsk1 $$
- ppr solve_this $$ ppr fsk2)
- ; emitNewDerivedEq loc Nominal (mkTyVarTy fsk1) (mkTyVarTy fsk2) }
- -- FunEqs are always at Nominal role
-
| otherwise -- Wanted
- = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fsk1 $$
- ppr solve_this $$ ppr fsk2)
+ = do { traceTcS "reactFunEq (Wanted/Derived)"
+ (vcat [ppr from_this, ppr fsk1, ppr solve_this, ppr fsk2])
; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
ppr solve_this $$ ppr fsk2) }
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index ba07ff8..17d9504 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1690,8 +1690,8 @@ data Ct
-- *never* over-saturated (because if so
-- we should have decomposed)
- cc_fsk :: TcTyVar -- [Given] always a FlatSkolTv
- -- [Wanted] always a FlatMetaTv
+ cc_fsk :: TcTyVar -- [G] always a FlatSkolTv
+ -- [W], [WD], or [D] always a FlatMetaTv
-- See Note [The flattening story] in TcFlatten
}
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 580a33c..f5d6ca9 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -3045,23 +3045,34 @@ demoteUnfilledFmv fmv
-----------------------------
dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
--- (dischargeFmv x fmv co ty)
+-- (dischargeFmv ev fmv co ty)
-- [W] ev :: F tys ~ fmv
-- co :: F tys ~ xi
-- Precondition: fmv is not filled, and fmv `notElem` xi
--- ev is Wanted
+-- ev is Wanted or Derived
--
--- Then set fmv := xi,
+-- Then for [W] or [WD], we actually fill in the fmv:
+-- set fmv := xi,
-- set ev := co
-- kick out any inert things that are now rewritable
--
--- Does not evaluate 'co' if 'ev' is Derived
+-- For [D], we instead emit an equality that must ultimately hold
+-- emit xi ~ fmv
+-- Does not evaluate 'co' if 'ev' is Derived
+--
+-- See TcFlatten Note [The flattening story],
+-- especially "Ownership of fsk/fmv"
dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
= ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
do { setWantedEvTerm dest (EvExpr (evCoercion co))
; unflattenFmv fmv xi
; n_kicked <- kickOutAfterUnification fmv
; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ pprKicked n_kicked) }
+
+dischargeFmv (CtDerived { ctev_loc = loc }) fmv _co xi
+ = emitNewDerivedEq loc Nominal xi (mkTyVarTy fmv)
+ -- FunEqs are always at Nominal role
+
dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev)
pprKicked :: Int -> SDoc
diff --git a/testsuite/tests/polykinds/T15170.hs b/testsuite/tests/polykinds/T15170.hs
new file mode 100644
index 0000000..a105ca5
--- /dev/null
+++ b/testsuite/tests/polykinds/T15170.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T15170 where
+
+import Data.Kind
+import Data.Proxy
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type f @@ x = Apply f x
+infixl 9 @@
+
+wat :: forall (a :: Type)
+ (b :: a ~> Type)
+ (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
+ (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
+ (x :: a).
+ (forall (xx :: a) (yy :: b @@ xx). Proxy (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))
+ -> ()
+wat _ = ()
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 7992e28..5aaa217 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -190,3 +190,4 @@ test('T14873', normal, compile, [''])
test('SigTvKinds3', normal, compile_fail, [''])
test('T15116', normal, compile_fail, [''])
test('T15116a', normal, compile_fail, [''])
+test('T15170', normal, compile, [''])
More information about the ghc-commits
mailing list