Opened 2 years ago

Closed 5 months ago

Last modified 4 months ago

#12442 closed bug (fixed)

Pure unifier usually doesn't need to unify kinds

Reported by: goldfire Owned by: goldfire
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType Cc: alpmestan
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 2 years ago.

Download all attachments as: .zip

Change History (12)

Changed 2 years ago by goldfire

Attachment: Effect.hs added

comment:1 Changed 2 years ago by goldfire

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

comment:2 Changed 2 years 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 22 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 22 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 22 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

comment:6 Changed 5 months ago by simonpj

Resolution: fixed
Status: closednew

Re-opening so Richard can attend to comment:5

comment:7 Changed 5 months ago by simonpj

Owner: set to goldfire

comment:8 Changed 5 months ago by Richard Eisenberg <rae@…>

In 34834234/ghc:

Comments in Unify, fixing #12442

[ci skip]

comment:9 Changed 5 months ago by goldfire

Resolution: fixed
Status: newclosed

Here's the Note:

Note [tcMatchTy vs tcMatchTyKi]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This module offers two variants of matching: with kinds and without.
The TyKi variant takes two types, of potentially different kinds,
and matches them. Along the way, it necessarily also matches their
kinds. The Ty variant instead assumes that the kinds are already
eqType and so skips matching up the kinds.

How do you choose between them?

1. If you know that the kinds of the two types are eqType, use
   the Ty variant. It is more efficient, as it does less work.

2. If the kinds of variables in the  template type might mention type families,
   use the Ty variant (and do other work to make sure the kinds
   work out). These pure unification functions do a straightforward
   syntactic unification and do no complex reasoning about type
   families. Note that the types of the variables in instances can indeed
   mention type families, so instance lookup must use the Ty variant.

   (Nothing goes terribly wrong -- no panics -- if there might be type
   families in kinds in the TyKi variant. You just might get match
   failure even though a reducing a type family would lead to success.)

3. Otherwise, if you're sure that the variable kinds to not mention
   type families and you're not already sure that the kind of the template
   equals the kind of the target, then use the TyKi version.

This is referenced from the various matcher functions. Sorry for letting this slip!

comment:10 Changed 4 months ago by alpmestan

Cc: alpmestan added

I ran ./validate --slow yesterday and T12442 is failing in all test ways:

   /tmp/ghctest-kabnnx7e/test   spaces/./dependent/should_compile/T12442.run                             T12442 [exit code non-0] (normal)
   /tmp/ghctest-kabnnx7e/test   spaces/./dependent/should_compile/T12442.run                             T12442 [exit code non-0] (hpc)
   /tmp/ghctest-kabnnx7e/test   spaces/./dependent/should_compile/T12442.run                             T12442 [exit code non-0] (optasm)
   /tmp/ghctest-kabnnx7e/test   spaces/./dependent/should_compile/T12442.run                             T12442 [exit code non-0] (profasm)
   /tmp/ghctest-kabnnx7e/test   spaces/./dependent/should_compile/T12442.run                             T12442 [exit code non-0] (optllvm)

Always with the same panic:

ghc: panic! (the 'impossible' happened)
  (GHC version 8.5.20180329 for x86_64-unknown-linux):
        ASSERT failed! file compiler/typecheck/TcTyClsDecls.hs, line 1531

This sounds like an actual problem, but if you don't mind I'll leave it to you Richard & Simon to decide/figure out whether this ticket should be re-opened or whether this is a new, unrelated problem that deserves its own ticket.

comment:11 Changed 4 months ago by alpmestan

Nevermind, I somehow got things wrong, this test passes with a fresh master from today.

Note: See TracTickets for help on using tickets.