#15549: Core Lint error with EmptyCase -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeFamilies, Resolution: | TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: goldfire (added) Comment: The culprit here appears to be [http://git.haskell.org/ghc.git/blob/21f0f56164f50844c2150c62f950983b2376f8b6... 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15549#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15549: Core Lint error with EmptyCase -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeFamilies, Resolution: | TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14729 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #14729 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15549#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15549: Core Lint error with EmptyCase -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeFamilies, Resolution: | TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14729 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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: {{{#!hs {-# 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] _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) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15549#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15549: Core Lint error with EmptyCase -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeFamilies, Resolution: | TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_compile/T15549[ab] Blocked By: | Blocking: Related Tickets: #14729 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/208 -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => merge * testcase: => typecheck/should_compile/T15549[ab] * milestone: 8.10.1 => 8.8.1 Comment: Landed in [https://gitlab.haskell.org/ghc/ghc/commit/2b90356d26b4699227816ad9424e766ecc... 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15549#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15549: Core Lint error with EmptyCase -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 8.4.3 checker) | Keywords: TypeFamilies, Resolution: | TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | typecheck/should_compile/T15549[ab] Blocked By: | Blocking: Related Tickets: #14729 | Differential Rev(s): Wiki Page: | https://gitlab.haskell.org/ghc/ghc/merge_requests/208 -------------------------------------+------------------------------------- Comment (by Marge Bot ): In [changeset:"2b90356d26b4699227816ad9424e766eccdb6c36/ghc" 2b90356d/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="2b90356d26b4699227816ad9424e766eccdb6c36" Fix #14729 by making the normaliser homogeneous This ports the fix to #12919 to the normaliser. (#12919 was about the flattener.) Because the fix is involved, this is done by moving the critical piece of code to Coercion, and then calling this from both the flattener and the normaliser. The key bit is: simplifying type families in a type is always a *homogeneous* operation. See #12919 for a discussion of why this is the Right Way to simplify type families. Also fixes #15549. test case: dependent/should_compile/T14729{,kind} typecheck/should_compile/T15549[ab] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15549#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler