[GHC] #16188: GHC HEAD-only panic (buildKindCoercion)

[GHC]

#16188: GHC HEAD-only panic (buildKindCoercion)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.8.1
       Component:  Compiler (Type    |              Version:  8.7
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Good catch.

 The culprit is here
 {{{
 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
   = case ev of
      ...

      CtWanted { ctev_dest = dest }
         -> do { traceTcS "canTCAppOk" (ppr bndrs $$ ppr (take 20 tc_roles)
 $$ ppr tys1 $$ ppr tys2)
               ; cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2
               ; setWantedEq dest (mkTyConAppCo role tc cos) }
      ...

   where
     loc        = ctEvLoc ev
     role       = eqRelRole eq_rel
     tc_roles   = tyConRolesX role tc

       -- the following makes a better distinction between "kind" and
 "type"
       -- in error messages
     bndrs      = tyConBinders tc
     is_kinds   = map isNamedTyConBinder bndrs
     is_viss    = map isVisibleTyConBinder bndrs

     kind_xforms = map (\is_kind -> if is_kind then toKindLoc else id)
 is_kinds
     vis_xforms  = map (\is_vis  -> if is_vis  then id
                                    else flip updateCtLocOrigin
 toInvisibleOrigin)
                       is_viss

     -- zipWith3 (.) composes its first two arguments and applies it to the
 third
     new_locs = zipWith3 (.) kind_xforms vis_xforms (repeat loc)
 }}}
 The equality we are solving is somthing like
 {{{
   [WD] hole{co_a1hC} {0}:: (Sing
                               @Bool
                               (Apply
                                  @(RegExp t_a1hn[sk:1])
                                  @Bool
                                  (ReNotEmptySym0 @t_a1hn[sk:1])
                                  re1_a1hs[ssk:2]) :: *)
                            GHC.Prim.~#
                            (Sing @Bool a_a1hg[tau:2] :: *)
 }}}
 Turns out that for `Sing`,
 * its `tyConBinders` is `[]`
 * so `bndrs` is `[]`
 * so `new_locs` is `[]`
 * so `cos` is `[]`
 and we make a coercion `Refl Sing`,ignoring the arguments to `Sing`!!
 Utterly bogus.

 The silent assumption of this code is that in `T ty1 .. tyn` then the
 `tyConBinders` of `T` has length at least `n`.  But that's not true
 for this data family; and in any case it might not be true of `K
 (*->*->*) Int Bool Char` where `K :: forall k. * -> k`; the number of
 of args depends on how you instantiate it.

 The only comment on this code is that it makes a "better distinction
 between kind and type", and I have no clue how it works.  Moreover, it
 looks terribly smelly: there's a `zipWith3` followed by a `zipWith4M`.  We
 can't ''really'' have seven things we want to zip!!

 Moreover the `zipWith3` is zipping two lists both constructed by `map`;
 and the arguments of those maps are ... more maps ... over the same thing,
 namely `bndrs`.  Lots of huff and puff to do very little.

 Richard: all this comes from
 {{{
 commit fb752133f45f01b27240d7cc6bce2063a015e51b
 Author: Richard Eisenberg <rae at cs.brynmawr.edu>
 Date:   Tue Jul 18 14:30:40 2017 -0400

     Track visibility in TypeEqOrigin
 }}}
 Could you possibly fix the bug, perhaps en route cleaning up the code and
 adding a Note with a concrete example to explain what is going on?
 Thanks!

 It might also be wise to ASSERT that that `cos` has the same length as
 `tys1` and `tys2`, which themselves should have the same length.

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