Opened 12 months ago
Last modified 6 months ago
#15549 merge bug
Core Lint error with EmptyCase
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.8.1 |
Component: | Compiler (Type checker) | Version: | 8.4.3 |
Keywords: | TypeFamilies, TypeInType | Cc: | goldfire |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time crash or panic | Test Case: | typecheck/should_compile/T15549[ab] |
Blocked By: | Blocking: | ||
Related Tickets: | #14729 | Differential Rev(s): | https://gitlab.haskell.org/ghc/ghc/merge_requests/208 |
Wiki Page: |
Description
The following program gives a Core Lint error on GHC 8.2.2 and later:
{-# LANGUAGE EmptyCase #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Kind import Data.Void data family Sing (a :: k) data V1 :: Type -> Type data instance Sing (z :: V1 p) class Generic a where type Rep a :: Type -> Type to :: Rep a x -> a class PGeneric a where type To (z :: Rep a x) :: a class SGeneric a where sTo :: forall x (r :: Rep a x). Sing r -> Sing (To r :: a) ----- instance Generic Void where type Rep Void = V1 to x = case x of {} type family EmptyCase (a :: j) :: k where instance PGeneric Void where type To x = EmptyCase x instance SGeneric Void where sTo x = case x of
$ /opt/ghc/8.4.3/bin/ghc Bug.hs -dcore-lint -fforce-recomp [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) *** Core Lint errors : in result of Simplifier *** Bug.hs:38:7: warning: [in body of lambda with binder x_aZ8 :: Sing r_a12q] Kind application error in coercion ‘(Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R’ Function kind = forall k. k -> * Arg kinds = [(V1 x_a12p, *), (r_a12q, Rep Void x_a12p)] Fun: V1 x_a12p (r_a12q, Rep Void x_a12p) Bug.hs:38:7: warning: [in body of lambda with binder x_aZ8 :: Sing r_a12q] Kind application error in coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’ Function kind = V1 x_a12p -> * Arg kinds = [(r_a12q, Rep Void x_a12p)] Fun: V1 x_a12p (r_a12q, Rep Void x_a12p) Bug.hs:38:7: warning: [in body of lambda with binder x_aZ8 :: Sing r_a12q] Kind application error in coercion ‘D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N’ Function kind = V1 x_a12p -> * Arg kinds = [(r_a12q, Rep Void x_a12p)] Fun: V1 x_a12p (r_a12q, Rep Void x_a12p) <no location info>: warning: In the type ‘R:SingV1z x_a12p r_a12q’ Kind application error in type ‘R:SingV1z x_a12p r_a12q’ Function kind = forall p -> V1 p -> * Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)] Fun: V1 x_a12p (r_a12q, Rep Void x_a12p) <no location info>: warning: In the type ‘R:SingV1z x_a12p r_a12q’ Kind application error in type ‘R:SingV1z x_a12p r_a12q’ Function kind = forall p -> V1 p -> * Arg kinds = [(x_a12p, *), (r_a12q, Rep Void x_a12p)] Fun: V1 x_a12p (r_a12q, Rep Void x_a12p) *** Offending Program *** <elided> $csTo_a12n :: forall x (r :: Rep Void x). Sing r -> Sing (To r) [LclId, Arity=1, Str=<L,U>x, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}] $csTo_a12n = \ (@ x_a12p) (@ (r_a12q :: Rep Void x_a12p)) (x_aZ8 :: Sing r_a12q) -> case x_aZ8 `cast` ((Sing (D:R:RepVoid[0] <x_a12p>_N) <r_a12q>_N)_R ; D:R:SingV1z0[0] <x_a12p>_N <r_a12q>_N :: (Sing r_a12q :: *) ~R# (R:SingV1z x_a12p r_a12q :: *)) of nt_s13T { }
GHC 8.0.2 does not appear to suffer from this Core Lint error.
Change History (11)
comment:1 Changed 12 months ago by
Summary: | Core Lint error with empty closed type family → Core Lint error with EmptyCase |
---|
comment:2 Changed 12 months ago by
Cc: | goldfire added |
---|
The culprit here appears to be improveSeq. In particular, in its use of topNormaliseType_maybe
:
improveSeq :: (FamInstEnv, FamInstEnv) -> SimplEnv -> OutExpr -> InId -> OutId -> [InAlt] -> SimplM (SimplEnv, OutExpr, OutId) -- Note [Improving seq] improveSeq fam_envs env scrut case_bndr case_bndr1 [(DEFAULT,_,_)] | Just (co, ty2) <- topNormaliseType_maybe fam_envs (idType case_bndr1) = do { case_bndr2 <- newId (fsLit "nt") ty2 ; let rhs = DoneEx (Var case_bndr2 `Cast` mkSymCo co) Nothing env2 = extendIdSubst env case_bndr rhs ; return (env2, scrut `Cast` co, case_bndr2) }
In the program in comment:1, scrut
is x
(from sTo
), and idType case_bndr1
is Sing (Rep Void) r
(where (r :: Rep Void)
). It's topNormaliseType_maybe
's job to reduce the two type families in Sing (Rep Void) r
(in particular, Rep Void ~# Void
and then Sing Void ~# R:SingVoidz
) and return the coercion that witnesses this reduction. However, it appears to produce an entirely bogus coercion:
Sing (D:R:RepVoid[0]) <r>_N)_R ; D:R:SingVoidz0[0] <r>_N :: (Sing (Rep Void) r) ~R# (R:SingVoidz r)
Why is this bogus? Because in the axiom D:R:SingVoidz0[0]
, we have:
COERCION AXIOMS axiom Bug.D:R:SingVoidz0 :: forall {z :: Void}. Sing Void z = Bug.R:SingVoidz -- Defined at ../Bug.hs:11:15
Notice that the argument to D:R:SingVoidz0[0]
is of type Void
, but in the coercion above, we're giving it r
as an argument, which is of type Rep Void
, not Void
! Unsurprisingly, utter pandemonium ensues when Core Lint inspects this garbage.
The proper coercion would be something like what the second program in comment:1 produces:
(Sing (D:R:RepVoid[0]) (GRefl nominal r (D:R:RepVoid[0])))_R ; D:R:SingVoidz0[0] <(r |> D:R:RepVoid[0])>_N :: (Sing (Rep Void) r :: *) ~R# (R:SingVoidz (r |> D:R:RepVoid[0]) :: *)
Alas, topNormaliseType_maybe
doesn't produce this. goldfire, do you think the reason that this doesn't happen is due to the same underlying reasons as in #14729? I strongly suspect that this is the case, since I tried calling normaliseType
on Sing (Rep Void) r
, and it produces the same bogus coercion that topNormaliseType_maybe
did.
comment:4 Changed 12 months ago by
Related Tickets: | → #14729 |
---|
comment:5 Changed 12 months ago by
Milestone: | 8.6.1 → 8.8.1 |
---|
comment:6 Changed 11 months ago by
Another program, identified in https://ghc.haskell.org/trac/ghc/ticket/15725#comment:7, which may suffer from the same problems as described in this ticket:
{-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind (Type) newtype Identity a = Identity a newtype Par1 a = Par1 a data family Sing :: forall k. k -> Type data instance Sing :: forall k. k -> Type type family Rep1 (f :: Type -> Type) :: Type -> Type type instance Rep1 Identity = Par1 type family From1 (z :: f a) :: Rep1 f a type instance From1 ('Identity x) = 'Par1 x und :: a und = und f :: forall (a :: Type) (x :: Identity a). Sing x f = g where g :: forall (a :: Type) (f :: Type -> Type) (x :: f a). Sing x g = seq (und :: Sing (From1 x)) und
*** Core Lint errors : in result of Simplifier *** Bug.hs:25:1: warning: [in body of lambda with binder x_a19R :: Identity a_a19Q] Kind application error in coercion ‘(Sing (D:R:Rep1Identity[0] <a_a19Q>_N) <From1 x_a19R>_N)_R’ Function kind = forall k. k -> * Arg kinds = [(Par1 a_a19Q, *), (From1 x_a19R, Rep1 Identity a_a19Q)] Fun: Par1 a_a19Q (From1 x_a19R, Rep1 Identity a_a19Q) Bug.hs:25:1: warning: [in body of lambda with binder x_a19R :: Identity a_a19Q] Kind application error in coercion ‘D:R:Singk0[0] <Par1 a_a19Q>_N <From1 x_a19R>_N’ Function kind = Par1 a_a19Q -> * Arg kinds = [(From1 x_a19R, Rep1 Identity a_a19Q)] Fun: Par1 a_a19Q (From1 x_a19R, Rep1 Identity a_a19Q) Bug.hs:25:1: warning: [in body of lambda with binder x_a19R :: Identity a_a19Q] Kind application error in coercion ‘D:R:Singk0[0] <Par1 a_a19Q>_N <From1 x_a19R>_N’ Function kind = Par1 a_a19Q -> * Arg kinds = [(From1 x_a19R, Rep1 Identity a_a19Q)] Fun: Par1 a_a19Q (From1 x_a19R, Rep1 Identity a_a19Q) <no location info>: warning: In the type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’ Kind application error in type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’ Function kind = forall k -> k -> * Arg kinds = [(Par1 a_a19Q, *), (From1 x_a19R, Rep1 Identity a_a19Q)] Fun: Par1 a_a19Q (From1 x_a19R, Rep1 Identity a_a19Q) <no location info>: warning: In the type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’ Kind application error in type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’ Function kind = forall k -> k -> * Arg kinds = [(Par1 a_a19Q, *), (From1 x_a19R, Rep1 Identity a_a19Q)] Fun: Par1 a_a19Q (From1 x_a19R, Rep1 Identity a_a19Q)
comment:7 Changed 8 months ago by
Milestone: | 8.8.1 → 8.10.1 |
---|
Bumping milestones of low-priority tickets.
comment:8 Changed 7 months ago by
Differential Rev(s): | → https://gitlab.haskell.org/ghc/ghc/merge_requests/208 |
---|---|
Status: | new → patch |
comment:9 Changed 6 months ago by
Milestone: | 8.10.1 → 8.8.1 |
---|---|
Status: | patch → merge |
Test Case: | → typecheck/should_compile/T15549[ab] |
Landed in 2b90356d26b4699227816ad9424e766eccdb6c36. (Given the complexity of this patch, I'm not sure if it's worth trying to merge to 8.8 or not.) Echoing https://ghc.haskell.org/trac/ghc/ticket/14729#comment:14, this is a merge candidate for 8.8.
comment:10 Changed 6 months ago by
For what it's worth it seems to apply cleanly to ghc-8.8
. Let's try merging.
Never mind, empty closed type families have nothing to do with this. Here's an even more minimal way to reproduce the Core Lint error:
However,
EmptyCase
does appear to play an important role. If I change the implementation ofsTo
to this:Then the Core Lint error goes away, and the generated Core for
sTo
instead becomes: