Opened 4 months ago
Closed 3 months ago
#15577 closed bug (fixed)
TypeApplications-related infinite loop (GHC 8.6+ only)
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | high | Milestone: | 8.6.1 |
Component: | Compiler (Type checker) | Version: | 8.5 |
Keywords: | TypeApplications, TypeInType | Cc: | simonpj |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time performance bug | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
The following program will loop infinitely when compiled on GHC 8.6 or HEAD:
{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind import Data.Type.Equality data family Sing :: forall k. k -> Type class Generic1 (f :: k -> Type) where type Rep1 f :: k -> Type class PGeneric1 (f :: k -> Type) where type From1 (z :: f a) :: Rep1 f a type To1 (z :: Rep1 f a) :: f a class SGeneric1 (f :: k -> Type) where sFrom1 :: forall (a :: k) (z :: f a). Sing z -> Sing (From1 z) sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a) class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k -> Type) where sTof1 :: forall (a :: k) (z :: f a). Sing z -> To1 (From1 z) :~: z sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> From1 (To1 r :: f a) :~: r foo :: forall (f :: Type -> Type) (a :: Type) (r :: Rep1 f a). VGeneric1 f => Sing r -> From1 (To1 r :: f a) :~: r foo x | Refl <- sFot1 -- Uncommenting the line below makes it work again: -- @Type @f @a @r x = Refl
This is a regression from GHC 8.4, since compiling this program with 8.4 simply errors:
$ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:35:20: 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 ‘foo’: Refl <- sFot1 @f @a @r x In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl | 35 | @f @a @r x | ^ Bug.hs:35:23: error: • Expected kind ‘f1 -> *’, but ‘a’ has kind ‘*’ • In the type ‘a’ In a stmt of a pattern guard for an equation for ‘foo’: Refl <- sFot1 @f @a @r x In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl • Relevant bindings include x :: Sing r1 (bound at Bug.hs:32:5) foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1) | 35 | @f @a @r x | ^ Bug.hs:35:26: error: • Couldn't match kind ‘* -> *’ with ‘*’ When matching kinds f1 :: * -> * Rep1 f1 a1 :: * Expected kind ‘f1’, but ‘r’ has kind ‘Rep1 f1 a1’ • In the type ‘r’ In a stmt of a pattern guard for an equation for ‘foo’: Refl <- sFot1 @f @a @r x In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl • Relevant bindings include x :: Sing r1 (bound at Bug.hs:32:5) foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1) | 35 | @f @a @r x | ^ Bug.hs:35:28: error: • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’ When matching kinds a1 :: * 'GHC.Types.LiftedRep :: GHC.Types.RuntimeRep • In the fourth argument of ‘sFot1’, namely ‘x’ In a stmt of a pattern guard for an equation for ‘foo’: Refl <- sFot1 @f @a @r x In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl • Relevant bindings include x :: Sing r1 (bound at Bug.hs:32:5) foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1) | 35 | @f @a @r x | ^ Bug.hs:36:5: error: • Could not deduce: From1 (To1 r1) ~ r1 from the context: r0 ~ From1 (To1 r0) bound by a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in a pattern binding in pattern guard for an equation for ‘foo’ at Bug.hs:33:5-8 ‘r1’ is a rigid type variable bound by the type signature for: foo :: forall (f1 :: * -> *) a1 (r1 :: Rep1 f1 a1). VGeneric1 f1 => Sing r1 -> From1 (To1 r1) :~: r1 at Bug.hs:(29,1)-(31,43) Expected type: From1 (To1 r1) :~: r1 Actual type: r1 :~: r1 • In the expression: Refl In an equation for ‘foo’: foo x | Refl <- sFot1 @f @a @r x = Refl • Relevant bindings include x :: Sing r1 (bound at Bug.hs:32:5) foo :: Sing r1 -> From1 (To1 r1) :~: r1 (bound at Bug.hs:32:1) | 36 | = Refl | ^^^^
Change History (7)
comment:1 Changed 4 months ago by
comment:2 Changed 4 months ago by
Cc: | simonpj added |
---|
This regression was introduced in commit a32c8f7514c8192fa064537fb93d5a5c224991a0 (Use dischargeFunEq consistently
).
comment:3 Changed 4 months ago by
I know what is happening here. In TcCanonical.canCFunEqCan
we have
canCFunEqCan ev fn tys fsk = do { (tys', cos, kind_co) <- flattenArgsNom ev fn tys -- cos :: tys' ~ tys ; let lhs_co = mkTcTyConAppCo Nominal fn cos -- :: F tys' ~ F tys new_lhs = mkTyConApp fn tys' flav = ctEvFlavour ev ; (ev', fsk') -- See Note [canCFunEqCan] <- if isTcReflCo kind_co then ..normal, homo-kinded case.. else ..hetero-kinded case.. ...
The note is a good explanation; read it.
In the example above, we get a Given CFunEqCan
that is homo-kinded.
But kind_co
turns out not to be ReflCo
but rather some giant (but still reflexive)
coercion. So we fall ito the heter-kinded case.
Then, as the Note says, we make a new homo-kinded CFunEqCan
. But
when we end up processing that (as we do), we think it too is hetero-kinded,
and so we do it all over again. Forever.
For now I have fixed it by using isTcReflexiveCo
instead of isTcReflCo
.
But isn't it suspicious that flattenArgsNom
returns a complicated giant coercion?
And that gets right back into flatten_args_fast
and flatten_args_slow
, which
we were discussing last week. I'll leave that for Richard and Ningning to ponder.
Meanwhile I think I have fixed the loop. Validating now....
Here for completeness is part of the log
canCFunEqCan: non-refl Kind co: (Sym (GRefl nominal (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) (Sym ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N))) ; (Sym (GRefl nominal a_a28l[sk:1] (({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N))) ; GRefl nominal a_a28l[sk:1] (({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)))) (Sym (GRefl nominal (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1] {co_a28p}) (Sym (Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}))) ; (Sym (GRefl nominal r_a28m[sk:1] (Sym {co_a28w} ; GRefl nominal f_a28k[sk:1] {co_a28p})) ; GRefl nominal r_a28m[sk:1] (Sym {co_a28w} ; GRefl nominal f_a28k[sk:1] {co_a28p}))) RHS: fsk_a29k[fsk:2] :: (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1] {co_a28p}) LHS: F (f_a28k[sk:1] |> {co_a28p}) (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1] {co_a28p}) r_a28x[tau:1] :: (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1] {co_a28p}) New LHS F (f_a28k[sk:1] |> {co_a28p}) (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1] {co_a28p}) r_a28x[tau:1] :: (a_a28l[sk:1] |> ({co_a29i} ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) ; ((Sym (GRefl nominal f_a28k[sk:1] {co_a28p}) ; GRefl nominal f_a28k[sk:1] {co_a28p}) ->_N <*>_N)) (r_a28m[sk:1] |> Sym {co_a28w} ; GRefl nominal f_a28k[sk:1] {co_a28p})
This shows stuff right at the start of the hetero-kinded 'else' branch above
kind_co
is the giant coercion returned byflattenArgsNom
RHS
is the fsk, and I show its kind, which is(a |> ..) (r |> ..)
LHS
is the original function application,(F tys)
in the code above; again I show its kind, which is identical to that of fks.
New LHS
is the new function application after flattening,(F tys')
in the code. You'll note that it is identical to(F tys)
!
All this work for nothing. Surely flattenArgsNom
can be a bit cleverer?
comment:5 Changed 3 months ago by
OK, I've committed a fix -- worth merging.
BUT please leave the ticket open.
Richard, Ningning: could you possibly look at whether there's a simple change to flatten_args
that would eliminate these giant coercions in the case where there is literally no flattening to be done?.
comment:6 Changed 3 months ago by
Status: | new → merge |
---|
Marking this as merge so that Ben will see it. (But, as simonpj notes in comment:5, don't actually close this ticket until Richard/Ningning has reviewed it.)
comment:7 Changed 3 months ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
Merged with 83ca9bb257ff9e0b9ebfa37ba1449118d15543a2.
Here's a somewhat smaller example: