diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-05-21 10:38:03 +0100 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-05-21 13:04:09 +0100 |
commit | 57858fc8b519078ae89a4859ce7588adb39f6e96 (patch) | |
tree | 49bda8417bb27285cd7e676221f0615740d557af | |
parent | b7e80ae005d0072eda79135c371a794dc48f70e1 (diff) | |
download | haskell-57858fc8b519078ae89a4859ce7588adb39f6e96.tar.gz |
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.
-rw-r--r-- | compiler/typecheck/TcFlatten.hs | 10 | ||||
-rw-r--r-- | compiler/typecheck/TcInteract.hs | 10 | ||||
-rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 4 | ||||
-rw-r--r-- | compiler/typecheck/TcSMonad.hs | 19 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T15170.hs | 26 | ||||
-rw-r--r-- | 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 e2244a99e6..32a9307d1c 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 ab94ad21bd..09cfd15a30 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 ba07ff8deb..17d9504f37 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 580a33cd9d..f5d6ca9aa7 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 0000000000..a105ca5344 --- /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 7992e283cd..5aaa217575 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, ['']) |