[GHC] #15142: GHC HEAD regression: tcTyVarDetails

[GHC]

#15142: GHC HEAD regression: tcTyVarDetails
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  goldfire
            Type:  bug               |               Status:  closed
        Priority:  highest           |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |             Keywords:  TypeInType,
      Resolution:  fixed             |  TypeFamilies, CUSKs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Compile-time      |            Test Case:  indexed-
  crash or panic                     |  types/should_compile/T15142
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Richard, I have augmented the Note as below. Do you agree with it?

 On the last point, we say that this does not have a CUSK (taken from
 `dependent/should_compile/kind_levels`):
 {{{
 data C :: B a -> *
 }}}
 But why not?  The lexical-forall rule means that it's equivalent to
 {{{
 data C :: forall a. B a -> *
 }}}
 which now does have a CUSK.  Either the rule needs more justification, or
 its over-restrictive.

 Here's the new Note:

 {{{
 {- Note [CUSKs: complete user-supplied kind signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We kind-check declarations differently if they have a complete, user-
 supplied
 kind signature (CUSK). This is because we can safely generalise a CUSKed
 declaration before checking all of the others, supporting polymorphic
 recursion.
 See
 ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference#Proposednewstrategy
 and #9200 for lots of discussion of how we got here.

 PRINCIPLE:
   a type declaration has a CUSK iff we could produce a separate kind
 signature
   for it, just like a type signature for a function,
   looking only at the header of the declaration.

 Examples:
   * data T1 (a :: *->*) (b :: *) = ....
     -- Has CUSK; equivalant to   T1 :: (*->*) -> * -> *

  * data T2 a b = ...
    -- No CUSK; we do not want to guess T2 :: * -> * -> *
    -- becuase the full decl might be   data T a b = MkT (a b)

   * data T3 (a :: k -> *) (b :: *) = ...
     -- CUSK; equivalent to   T3 :: (k -> *) -> * -> *
     -- We lexically generalise over k to get
     --    T3 :: forall k. (k -> *) -> * -> *
     -- The generalisation is here is purely lexical, just like
     --    f3 :: a -> a
     -- means
     --    f3 :: forall a. a -> a

   * data T4 (a :: j k) = ...
      -- CUSK; equivalent to   T4 :: j k -> *
      -- which we lexically generalise to  T4 :: forall j k. j k -> *
      -- and then, if PolyKinds is on, we further generalise to
      --   T4 :: forall kk (j :: kk -> *) (k :: kk). j k -> *
      -- Again this is exactly like what happens as the term level
      -- when you write
      --    f4 :: forall a b. a b -> Int

 NOTE THAT
   * A CUSK does /not/ mean that everything about the kind signature is
     fully specified by the user.  Look at T4 and f4: we had do do kind
     inference to figure out the kind-quantification.  But in both cases
     (T4 and f4) that inference is done looking /only/ at the header of T4
     (or signature for f4), not at the definition thereof.

   * The CUSK completely fixes the kind of the type constructor, forever.

   * The precise rules, for each declaration form, for whethher a
 declaration
     has a CUSK are given in the user manual section "Complete user-
 supplied
     kind signatures and polymorphic recursion".  BUt they simply implement
     PRINCIPLE above.

   * Open type families are interesting:
       type family T5 a b :: *
     There simply /is/ no accompanying declaration, so that info is all
     we'll ever get.  So we it has a CUSK by definition, and we default
     any un-fixed kind variables to *.

   * Associated types are a bit tricker:
       class C6 a where
          type family T6 a b :: *
          op :: a Int -> Int
     Here C6 does not have a CUSK (in fact we ultimately discover that
     a :: * -> *).  And hence neither does T6, the associated family,
     because we can't fix its kind until we have settled C6.  Another
     way to say it: unlike a top-level, we /may/ discover more about
     a's kind from C6's definition.

   * A data definition with a top-level :: must explicitly bind all
     kind variables to the right of the ::. See test
     dependent/should_compile/KindLevels, which requires this
     case. (Naturally, any kind variable mentioned before the :: should
     not be bound after it.)
 }}}

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