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

29 Feb 2016

      #11648: assertPprPanic, called at compiler/types/TyCoRep.hs:1932
-------------------------------------+-------------------------------------
        Reporter:  thomie            |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.0.1
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:
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 simonpj):

 Here's a smaller test case for the polykinds error
 {{{
 class Monoidy (to :: k0 -> k1 -> *) (m :: k1)  where
   type MComp to m :: k1 -> k1 -> k0
   mjoin :: MComp to m m m `to` m
 }}}
 The problem is this:

 * `TcTyClsDecls.getFamDeclInitialKind` thinks that `MComp` has a CUSK.

 * When it quantifies over it, it gives it the kind:
 {{{
   MComp :: forall k1_aLj[sk] (k0_aLi[sk] :: TYPE t_aSB[tau:1]).
            (k0_aLi[sk] -> k1_aLj[sk] -> *)
            -> k1_aLj[sk] -> k1_aLj[sk] -> k1_aLj[sk] -> k0_aLi[sk]
 }}}
   This is wrong: the `t_aSB` should be instantiated to `Lifted`.  It's
 terrible for a meta-tyvar to end up in the kind of a `TyCon`.

 * So I'm worried about where this defaulting happens in
 `TcHsType.kcHsTyVarBndrs` with `cusk` = True.  Indeed, by adding tracing
 to this program I've confirmed that `Monoidy` also gets a kind (at least
 during kind-checking) looking like
 {{{
 forall (k1{tv aLi} [sk] :: *)
        ((k0{tv aLh} [sk] :: TYPE{(w) tc 32Q}
                                 (t_aSs{tv} [tau:1] :: RuntimeRep{(w) tc
 334}))
         :: TYPE{(w) tc 32Q} (t_aSs{tv} [tau:1] :: RuntimeRep{(w) tc
 334})).
        ((k0{tv aLh} [sk] :: TYPE{(w) tc 32Q}
                                (t_aSs{tv} [tau:1] :: RuntimeRep{(w) tc
 334}))
            -> (k1{tv aLi} [sk] :: *) -> *{(w) tc 330})
        -> (k1{tv aLi} [sk] :: *)
        -> Constraint{(w) tc 32Y}

 }}}
   Notice that `t_aSB`.

 But even if we fix that I'm worried about doing this CUSK stuff for
 associated types.   I think it's probably wrong.  We are crawling over the
 class decl to find constraints on the kind variables so we can infer the
 class decl's kind.  We start that process with `getInitialKinds`; and we
 can't at that moment quantify over the kind variables we are about to
 gather constraints for!

 At very least we must elaborate `Note [Complete user-supplied kind
 signatures]` to cover associated types.  An associate type should have a
 CUSK iff (a) its parent class does, and (b) any private tyvars have kind
 sigs.

 I'm a bit puzzled about why we call `kcTyClDecl` and `generaliseTCD` ''at
 all'' for decls with a CUSK.

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