Commit 83ca9bb2 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari

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?

(cherry picked from commit 2e226a46)
parent 8344588e
......@@ -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'
......
{-# 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
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
a1 :: *
f1 :: * -> *
• 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)
......@@ -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'])
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