#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