[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