Opened 19 months ago

Last modified 6 months ago

#14729 merge bug (fixed)

normaliseType is not well-kinded

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.2.2
Keywords: Cc: RyanGlScott, Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: dependent/should_compile/T14729{,kind}
Blocked By: Blocking:
Related Tickets: #15549 Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/208
Wiki Page:

Description

Suppose we have

Proxy :: forall k. k -> Type

type family F a
type instance F Int = Bool

and we're trying to normalise the target

Proxy (F Int) x

Clearly, for this target to be well kinded, we need x :: F Int. Currently, the output of normaliseType is Proxy Bool x, which is just plain wrong.

I need to implement logic like in flatten_args on my branch in normaliseType to fix this.

Change History (17)

comment:1 Changed 19 months ago by RyanGlScott

Cc: RyanGlScott added

comment:2 Changed 19 months ago by Iceland_jack

Cc: Iceland_jack added

comment:3 Changed 12 months ago by RyanGlScott

See #15549 for a program which fails Core Lint due to this issue.

comment:4 Changed 12 months ago by simonpj

It'd be great to fix this -- and document the invariant on normaliseType, namely that the result has the same kind as its argument.

As I understand it, that's entirely consistent with our new (and now implemented in HEAD) story, that flattening does not change the kind of the type being flattened.

Richard: are you up for doing this? I assume that the "my branch" part is now water under the bridge, because the new flattening stuff is done.

comment:5 Changed 12 months ago by RyanGlScott

Milestone: 8.8.1

comment:6 Changed 8 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

comment:7 Changed 8 months ago by osa1

Bumping milestones of low-priority tickets.

comment:8 Changed 7 months ago by RyanGlScott

Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/208
Status: newpatch

comment:9 Changed 7 months ago by simonpj

Hang on. It's possible that the patch for #16188 fixes this one too -- but the underlying cause of this ticket in normaliseType remains. Richard has an entirely separate (and sadly more substantial) patch for that, which he and I went through on Friday.

comment:10 Changed 7 months ago by RyanGlScott

Status: patchnew

Sorry! The description in https://gitlab.haskell.org/ghc/ghc/merge_requests/208 very strongly implies that it fixes this ticket, so I was just following suit.

comment:11 Changed 7 months ago by simonpj

Oh my bad. MR!208 is indeed the right one for this ticket. I was just mixed up.

comment:12 Changed 7 months ago by RyanGlScott

Status: newpatch

comment:13 Changed 6 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: dependent/should_compile/T14729{,kind}, 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.)

comment:14 Changed 6 months ago by goldfire

Status: closedmerge

I think we should merge if possible. While complex, the changes are local to just a few places, and these places don't get a ton of traffic (because they're rather challenging to update).

comment:15 Changed 6 months ago by RyanGlScott

Milestone: 8.10.18.8.1

comment:16 Changed 6 months ago by RyanGlScott

Test Case: dependent/should_compile/T14729{,kind}, typecheck/should_compile/T15549[ab]dependent/should_compile/T14729{,kind}

comment:17 Changed 6 months ago by Marge Bot <ben+marge-bot@…>

In 2b90356d/ghc:

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]
Note: See TracTickets for help on using tickets.