diff options
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 20 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T15577.hs | 21 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T15577.stderr | 71 | ||||
| -rw-r--r-- | 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 d6aed31ab0..201504d010 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 0000000000..18ebc42f92 --- /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 0000000000..fef17090f8 --- /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 3e37205e15..ae4ee51a21 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']) |