Re: [GHC] #15592: Type families without CUSKs cannot be given visible kind variable binders

3 Oct 2018

      #15592: Type families without CUSKs cannot be given visible kind variable binders
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.8.1
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
                                     |  TypeApplications, TypeFamilies,
                                     |  CUSKs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:  14880             |             Blocking:
 Related Tickets:  #15591            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Ha ha. I looked at this too.  Consider
 {{{
 data T f (a::k1) b = MkT (f a b)
 }}}
 Then we should get
 {{{
 T :: forall {k2} k1. (k1 -> k2 -> *) -> k1 -> k2 -> *
 }}}
 That is: `k2` is `Inferred` but `k1` is `Specified`.  But ''neither'' is
 among
 the `tc_binders` of the `TcTyCon` that we make before kind-generalisation!
 Those `tc_binders` are only the `Required` ones, positionally written by
 the user.
 (It took me a while to work this out; we should write it down.)

 OK so `kindGeneralize` will now generalise over both `k1` and `k1`, in
 some
 random order.  We must

 * Mark the `Inferred` ones as `Inferred` and similarly `Specified`.
 * Put the former before the latter

 How can we distinguish?  Well, the `Specified` ones are among the
 `tcScopedTyVars` of the `TcTyCon`,
 but the `Inferred` ones are not.
 So I did this, in `kcTyClGroup`:
 {{{
            ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind)

            ; scoped_tvs' <- zonkTyVarTyVarPairs scoped_tvs
            ; let (specified_kvs, inferred_kvs) = partition is_specified
 kvs
                  user_specified_tkvs = mkVarSet (map snd scoped_tvs')
                  is_specified kv = kv `elemVarSet` user_specified_tkvs
                  all_binders = mkNamedTyConBinders Inferred  inferred_kvs
 ++
                                mkNamedTyConBinders Specified specified_kvs
 ++
                                tc_binders
 }}}
 This works.

 I will not commit: over to you Richard.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15592#comment:7
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler