[GHC] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

GHC ghc-devs at haskell.org
Tue Nov 7 01:48:01 UTC 2017


#14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14331
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 Most of the arcane knowledge is just knowledge of Haskell. The rest is but
 a small epsilon... :)

 There are basically two families of zonking functions:

 1. The functions defined in `TcMType` do an intermediate zonk. They
 squeeze out filled-in metavariables but don't run into trouble (or do
 anything, really) if they encounter an unfilled metavariable. The most
 frequently called function from this family is `zonkTcType`. These
 functions are needed during type-checking when, say, we are about to look
 at the free variables of something. Doing that without zonking first might
 give wrong information.

 2. The functions defined in `TcHsSyn` (such as `zonkTcTypeToType`) do a
 final zonk. If one of these functions encounters a metavariable, that
 metavariable is zonked to `Any` (most of the time -- details unimportant
 at the moment). This zonking happens when desugaring the type-checked
 program into Core; it also happens when building tycons from user-written
 type declarations.

 The basic idea is that we would like to consider `TcType` and `Type` as
 two separate types; the former lives in the type-checker and the latter
 lives in Core. `zonkTcType` both takes and returns a `TcType`.
 `zonkTcTypeToType` takes a `TcType` and returns a `Type`.

 As for `zonkQuantifiedTyVar`: that does more than just zonk -- it also
 skolemizes. (That is, it takes an unfilled metavariable and turns it into
 a skolem, which is useful when you're about to generalize.) Contrast with
 `zonkTyBndrX` (part of the final zonk), which ''expects'' a skolem to
 begin with.

 I remember it took years before I finally grokked zonking. And now I can't
 tell you why it seemed so hard!

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#comment:50>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler


More information about the ghc-tickets mailing list