[commit: ghc] master: canCFunEqCan: use isTcReflexiveCo (not isTcReflCo) (2e226a4)
git at git.haskell.org
git at git.haskell.org
Mon Sep 3 08:06:25 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/2e226a46c422c12f78dc3d3f62fe5a15e22bd986/ghc
>---------------------------------------------------------------
commit 2e226a46c422c12f78dc3d3f62fe5a15e22bd986
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Mon Sep 3 09:00:49 2018 +0100
canCFunEqCan: use isTcReflexiveCo (not isTcReflCo)
As Trac #15577 showed, it was possible for a /homo-kinded/
constraint to trigger the /hetero-kinded/ branch of canCFunEqCan,
and that triggered an infinite loop.
The fix is easier, but there remains a deeper questions: why is
the flattener producing giant refexive coercions?
>---------------------------------------------------------------
2e226a46c422c12f78dc3d3f62fe5a15e22bd986
compiler/typecheck/TcCanonical.hs | 20 ++++++++--
testsuite/tests/polykinds/T15577.hs | 21 ++++++++++
testsuite/tests/polykinds/T15577.stderr | 71 +++++++++++++++++++++++++++++++++
testsuite/tests/polykinds/all.T | 1 +
4 files changed, 109 insertions(+), 4 deletions(-)
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index d6aed31..201504d 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1714,6 +1714,11 @@ the new one, so we use dischargeFmv. This also kicks out constraints
from the inert set; this behavior is correct, as the kind-change may
allow more constraints to be solved.
+We use `isTcReflexiveCo`, to ensure that we only use the hetero-kinded case
+if we really need to. Of course `flattenArgsNom` should return `Refl`
+whenever possible, but Trac #15577 was an infinite loop because even
+though the coercion was homo-kinded, `kind_co` was not `Refl`, so we
+made a new (identical) CFunEqCan, and then the entire process repeated.
-}
canCFunEqCan :: CtEvidence
@@ -1733,13 +1738,20 @@ canCFunEqCan ev fn tys fsk
flav = ctEvFlavour ev
; (ev', fsk')
- -- See Note [canCFunEqCan]
- <- if isTcReflCo kind_co
- then do { let fsk_ty = mkTyVarTy fsk
+ <- if isTcReflexiveCo kind_co -- See Note [canCFunEqCan]
+ then do { traceTcS "canCFunEqCan: refl" (ppr new_lhs $$ ppr lhs_co)
+ ; let fsk_ty = mkTyVarTy fsk
; ev' <- rewriteEqEvidence ev NotSwapped new_lhs fsk_ty
lhs_co (mkTcNomReflCo fsk_ty)
; return (ev', fsk) }
- else do { (ev', new_co, new_fsk)
+ else do { traceTcS "canCFunEqCan: non-refl" $
+ vcat [ text "Kind co:" <+> ppr kind_co
+ , text "RHS:" <+> ppr fsk <+> dcolon <+> ppr (tyVarKind fsk)
+ , text "LHS:" <+> hang (ppr (mkTyConApp fn tys))
+ 2 (dcolon <+> ppr (typeKind (mkTyConApp fn tys)))
+ , text "New LHS" <+> hang (ppr new_lhs)
+ 2 (dcolon <+> ppr (typeKind new_lhs)) ]
+ ; (ev', new_co, new_fsk)
<- newFlattenSkolem flav (ctEvLoc ev) fn tys'
; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
-- sym lhs_co :: F tys ~ F tys'
diff --git a/testsuite/tests/polykinds/T15577.hs b/testsuite/tests/polykinds/T15577.hs
new file mode 100644
index 0000000..18ebc42
--- /dev/null
+++ b/testsuite/tests/polykinds/T15577.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy
+import Data.Type.Equality
+
+type family F (x :: f (a :: k)) :: f a
+
+f :: forall k (f :: k -> Type) (a :: k) (r :: f a). Proxy r -> F r :~: r
+f = undefined
+
+g :: forall (f :: Type -> Type) (a :: Type) (r :: f a). Proxy r -> F r :~: r
+g r | Refl <- f -- Uncommenting the line below makes it work again
+ -- @Type
+ @f @a @r r
+ = Refl
diff --git a/testsuite/tests/polykinds/T15577.stderr b/testsuite/tests/polykinds/T15577.stderr
new file mode 100644
index 0000000..fef1709
--- /dev/null
+++ b/testsuite/tests/polykinds/T15577.stderr
@@ -0,0 +1,71 @@
+
+T15577.hs:20:18: error:
+ • Expecting one more argument to ‘f’
+ Expected a type, but ‘f’ has kind ‘* -> *’
+ • In the type ‘f’
+ In a stmt of a pattern guard for
+ an equation for ‘g’:
+ Refl <- f @f @a @r r
+ In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+
+T15577.hs:20:21: error:
+ • Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’
+ • In the type ‘a’
+ In a stmt of a pattern guard for
+ an equation for ‘g’:
+ Refl <- f @f @a @r r
+ In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+ • Relevant bindings include
+ r :: Proxy r1 (bound at T15577.hs:18:3)
+ g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
+
+T15577.hs:20:24: error:
+ • Couldn't match kind ‘* -> *’ with ‘*’
+ When matching kinds
+ f1 :: * -> *
+ f1 a1 :: *
+ Expected kind ‘f1’, but ‘r’ has kind ‘f1 a1’
+ • In the type ‘r’
+ In a stmt of a pattern guard for
+ an equation for ‘g’:
+ Refl <- f @f @a @r r
+ In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+ • Relevant bindings include
+ r :: Proxy r1 (bound at T15577.hs:18:3)
+ g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
+
+T15577.hs:20:26: error:
+ • Couldn't match kind ‘* -> *’ with ‘*’
+ When matching kinds
+ f1 :: * -> *
+ a1 :: *
+ • In the fourth argument of ‘f’, namely ‘r’
+ In a stmt of a pattern guard for
+ an equation for ‘g’:
+ Refl <- f @f @a @r r
+ In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+ • Relevant bindings include
+ r :: Proxy r1 (bound at T15577.hs:18:3)
+ g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
+
+T15577.hs:21:7: error:
+ • Could not deduce: F r1 ~ r1
+ from the context: r0 ~ F r0
+ bound by a pattern with constructor:
+ Refl :: forall k (a :: k). a :~: a,
+ in a pattern binding in
+ a pattern guard for
+ an equation for ‘g’
+ at T15577.hs:18:7-10
+ ‘r1’ is a rigid type variable bound by
+ the type signature for:
+ g :: forall (f1 :: * -> *) a1 (r1 :: f1 a1).
+ Proxy r1 -> F r1 :~: r1
+ at T15577.hs:17:1-76
+ Expected type: F r1 :~: r1
+ Actual type: r1 :~: r1
+ • In the expression: Refl
+ In an equation for ‘g’: g r | Refl <- f @f @a @r r = Refl
+ • Relevant bindings include
+ r :: Proxy r1 (bound at T15577.hs:18:3)
+ g :: Proxy r1 -> F r1 :~: r1 (bound at T15577.hs:18:1)
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 3e37205..ae4ee51 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -192,3 +192,4 @@ test('T15116', normal, compile_fail, [''])
test('T15116a', normal, compile_fail, [''])
test('T15170', normal, compile, [''])
test('T14939', normal, compile, ['-O'])
+test('T15577', normal, compile_fail, ['-O'])
More information about the ghc-commits
mailing list