Re: [GHC] #15795: Core lint error with unused kind variable in data type return kind

21 Dec 2018

      #15795: Core lint error with unused kind variable in data type return kind
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.1
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  tests/polykinds/T15795, T15795a
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * testcase:   => tests/polykinds/T15795, T15795a

Comment:

 Great test cases thank you.

 The cause was that `candidateQTyVars` was returning tyvars with unzonked
 kinds, and that meant we put the binders in the wrong dependency order.
 Once that happens, chaos results.

 The fix is easy, but a bit tiresome. Richard you might want to look.  The
 key point it this (in `TcMType`).
 {{{
     go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv
       | tv `elemDVarSet` kvs = return dv  -- We have met this tyvar aleady
       | not is_dep
       , tv `elemDVarSet` tvs = return dv  -- We have met this tyvar aleady
       | otherwise
       = do { tv_kind <- zonkTcType (tyVarKind tv)
                  -- This zonk is annoying, but it is necessary, both to
                  -- ensure that the collected candidates have zonked kinds
                  -- (Trac #15795) and to make the naughty check
                  -- (which comes next) works correctly
            ; if intersectsVarSet bound (tyCoVarsOfType tv_kind)

 }}}
 Now from the two test cases we get the following results.

 From comment:5 (immortalised as `polykinds/T15795` we get
 {{{
 TYPE CONSTRUCTORS
   type synonym KindOf{2} :: forall k. k -> *
     roles nominal phantom
   data type T{3} :: forall j (a :: j). KindOf @j a -> *
     roles nominal nominal phantom
 DATA CONSTRUCTORS
   MkT :: forall k (b :: k). T @k @(GHC.Types.Any @k) b
 }}}
 From comment:2 (immortalised as `polykinds/T15795a` we get
 {{{
 TYPE CONSTRUCTORS
   data type F{3} :: forall ob1 (cat1 :: ob1). ob1 -> *
     roles nominal nominal phantom
 DATA CONSTRUCTORS
   Prod :: forall u (a :: u). F @u @(GHC.Types.Any @u) a
 }}}
 Note the use of `Any`, which I think is right.

 Richard/Ryan: just check?  Then close.

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