#12442: Pure unifier usually doesn't need to unify kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2433 Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => patch * differential: => Phab:D2433 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12442#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12442: Pure unifier usually doesn't need to unify kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2433 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"9766b0c81476c208b2b29ff66d97251209a79707/ghc" 9766b0c/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="9766b0c81476c208b2b29ff66d97251209a79707" 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. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12442#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12442: Pure unifier usually doesn't need to unify kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: TypeInType 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: | -------------------------------------+------------------------------------- Comment (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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12442#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12442: Pure unifier usually doesn't need to unify kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType 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: | -------------------------------------+------------------------------------- Changes (by simonpj): * owner: (none) => goldfire -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12442#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12442: Pure unifier usually doesn't need to unify kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: TypeInType 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: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => fixed Comment: 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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12442#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#12442: Pure unifier usually doesn't need to unify kinds -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: fixed | Keywords: TypeInType 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: | -------------------------------------+------------------------------------- Comment (by alpmestan): Nevermind, I somehow got things wrong, this test passes with a fresh master from today. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12442#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler