Opened 14 months ago

Closed 12 months ago

Last modified 12 months ago

#12442 closed bug (fixed)

Pure unifier usually doesn't need to unify kinds

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: dependent/should_compile/T12442
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D2433
Wiki Page:

Description

The pure unifier (in types/Unify.hs) is used to match up instances with actual types. Since GHC 8, it matches up the kinds with the types in a separate pass. But this is often wasteful, and sometimes downright wrong.

It's wasteful because most invocations of the unifier on a list of types pass in well-kinded arguments to some type constructor. Because the kinds of type constructors are closed, if we process the list left-to-right, we will always unify the kinds of later arguments before we get to them. So we shouldn't take another pass on the kinds.

It's wrong because it's conceivable for the kind to include a type family application, and using a type family application as a template in the pure unifier is very silly, indeed.

I cam across this while trying to translate Idris's algebraic effects library to Haskell. My reduced test case is attached.

Patch on the way.

Attachments (1)

Effect.hs (1.7 KB) - added by goldfire 14 months ago.

Download all attachments as: .zip

Change History (6)

Changed 14 months ago by goldfire

Attachment: Effect.hs added

comment:1 Changed 14 months ago by goldfire

Differential Rev(s): Phab:D2433
Status: newpatch

comment:2 Changed 13 months ago by simonpj

Status (see Phab:D2433 comment): Richard says: Please don't merge yet. When I validated, there were some hiccups, including around performance. IIRC, there were actually three performance improvements along with one regression, but I have to investigate properly. (A performance improvement is certainly not unexpected with this patch.) When I saw these problems, I prioritized other tasks, but will return to this eventually.

comment:3 Changed 12 months ago by Richard Eisenberg <rae@…>

In 9766b0c/ghc:

Fix #12442.

The problem is described in the ticket.

This patch adds new variants of the access points to the pure
unifier that allow unification of types only when the caller
wants this behavior. (The unifier used to also unify kinds.)
This behavior is appropriate when the kinds are either already
known to be the same, or the list of types provided are a
list of well-typed arguments to some type constructor. In the
latter case, unifying earlier types in the list will unify the
kinds of any later (dependent) types.

At use sites, I went through and chose the unification function
according to the criteria above.

This patch includes some modest performance improvements as we
are now doing less work.

comment:4 Changed 12 months ago by goldfire

Resolution: fixed
Status: patchclosed
Test Case: dependent/should_compile/T12442

Finally got around to dotting the i's and crossing the t's here.

We're all set.

I don't think this is worth merging.

comment:5 Changed 12 months ago by simonpj

Richard there are no comments to explain what is going on here.

The brief comments that are there suggest that it's just an efficiency thing: when unifying t1 :: k1 with t2 :: k2, if you happen to know that t1 = t2 (in the eqType, defnitional equality sense) then no need to match them. Saves work.

But there is much more to it than that! You say, cryptically, that "sometimes it is downright wrong". But you need to say that in the code, and support it with a few examples that demonstrate how wrong it is, and justify the cases where you use the laxer matching.

Could you do that? This is subtle stuff, and I'm anxious about making it robust to future modification.

Also, all the remaining calls to tcMatchTy now have to guarantee an invariant, that the kinds are eqType. I see nothing at the calls sites drawing attention to that claim, and justifying why, at that call site, it holds.

Simon

Note: See TracTickets for help on using tickets.