[GHC] #11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932

[GHC]

#11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932
-------------------------------------+-------------------------------------
        Reporter:  thomie            |                Owner:  goldfire
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.0.1
       Component:  Compiler          |              Version:  8.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):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 This is making yet more sense. And it seems that you are proposing:

 * INVARIANT: The kind of a quantified type variable has no meta-tyvars.

 We already had that the quantified type variable itself must not be a
 meta-tyvar. But this invariant goes one step further, in that the set of
 variables reachable from a quantified tyvar must be devoid of meta-tyvars.
 Do you agree with this invariant?

 And, as for design, it seems you are proposing (forgetting about
 associated types for the moment):

 * Keep the syntactic definition of CUSK as it is (Note [Complete user-
 supplied kind signatures] in HsDecls).
 * When a declaration has a CUSK, default any remaining meta-tyvars after
 `getInitialKind`.
 * If a meta-tyvar is not defaultable, the program is erroneous.

 I'm quite dubious of this design for several reasons. First, this seems
 strange to users. For example:

 {{{
 data T1 (a :: Proxy k)
 data T2 (a :: Proxy k) b
 }}}

 `T1` has a CUSK, according to our definition. Thus its `k` will be
 defaulted to kind `*`. `T2`, though, does not have a CUSK, and so `k` is
 not defaulted and has kind `k2`.

 Second, the design seems hard to implement without annoying users. For
 example:

 {{{
 data T3 (x :: * -> *)
 data T4 (a :: T3 k)
 }}}

 `T4` has a CUSK, and `k` should clearly have kind `* -> *`. But we can't
 discover that until `kcTyClDecl`, which is too late. According to the last
 bullet above, we'll fail at defaulting `T4`'s `k`'s kind and issue an
 error, even though it's quite obvious what we should do.

 So, I must ask: why is it so necessary to have the INVARIANT at the top? I
 understand this requires expanding the in-scope set for the substitution
 at hand, but why is that problematic? I don't see what's so bad about a
 meta-tyvar in a quantified variable's kind.

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