[GHC] #14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal

[GHC]

#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal
-------------------------------------+-------------------------------------
        Reporter:  hvr               |                Owner:  bgamari
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.1
       Component:  Compiler          |              Version:  8.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14236            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Here is what is happening.   The bug happens in `SpecConstr` when
 compiling `libraries/base/./Data/Typeable/Internal.hs` with `-O2`.  When I
 re-apply the patch "Typeable: Allow App to match arrow types" I get a Lint
 error as before.  Here's why:

 We have
 {{{
 mkTrApp_Xjt [Occ=LoopBreaker]
   :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
      TypeRep a -> TypeRep b -> TypeRep (a b)
 }}}
 and an application thereof looking like
 {{{
 mkTrApp_Xjt
   @ (TYPE (b_a3TI |> Nth:2 (Sym cobox_a3TS)))
   @ (TYPE (b_X444 |> Nth:2 (Sym cobox_X44r))
      -> *)
   @ (->)
   @ (b_X4hY |> Sym (cobox_a3TT (Coh (Sym (Coh <b_a3TI>_N
                                               (Nth:2
                                                    (Sym cobox_a3TS))))
                                     (Nth:2
                                          (Sym cobox_a3TS)) ; Coh
 <b_a3TI>_N
                                                                  (Nth:2
                                                                       (Sym
 cobox_a3TS))) ; Sym cobox_a3TJ))
   (Data.Typeable.Internal.TrTyCon
      @ (TYPE
           (b_a3TI |> Nth:2
                          (Sym cobox_a3TS))
         -> TYPE
              (b_X444 |> Nth:2
                             (Sym cobox_X44r))
         -> *)
      @ (->)
      dt_a2Xi
      dt_a2Xj
      GHC.Types.$tc(->)
      kind_vars_X3a2)
   (ds_X4ZX
    `cast` (<blah> :: (TypeRep b_X4hY :: *)
               ~R# (TypeRep
                      (b_X4hY |> cobox_a3TJ
                       ; Sym cobox_a3TT (Sym (Coh <b_a3TI>_N (Nth:2 (Sym
 cobox_a3TS)))
                                         ; Sym (Coh (Sym (Coh <b_a3TI>_N
 (Nth:2 (Sym cobox_a3TS))))
                                                    (Nth:2 (Sym
 cobox_a3TS))))) :: *)))
 }}}
 So `SpecConstr` tries to specialise `mkTrApp_Xjt` for this call; in
 particular the `TrTyCon` argument.  Very good.

 But the rule we get is this
 {{{
 RULES: "SC:mkTrApp0"
            forall (@ k1_X4hU)
                   (@ (b_X4hY :: k1_X4hU))
                   (@ k1_X440)
                   (@ (b_X444 :: k1_X440))
                   (@ k1_a3TG)
                   (@ (b_a3TI :: k1_a3TG))
                   (sc_s7Yv
                      :: TypeRep
                           (b_X4hY |> cobox_a3TJ ; Sym cobox_a3TT (Sym (Coh
 <b_a3TI>_N
 (Nth:2
 (Sym cobox_a3TS))) ; Sym (Coh (Sym (Coh <b_a3TI>_N
 (Nth:2
 (Sym cobox_a3TS))))
 (Nth:2
 (Sym cobox_a3TS))))))
                   (cobox_X44r
                      :: (RuntimeRep -> * :: *) ~# (k1_X440 -> * :: *))
                   (sc_s7Yr :: Word#)
                   (sc_s7Ys :: Word#)
                   (sc_s7Yt :: [SomeTypeRep])
                   (cobox_a3TS
                      :: (RuntimeRep -> * :: *) ~# (k1_a3TG -> * :: *)).
              mkTrApp_Xjt @ (TYPE
                               (b_a3TI |> <(type pat) k1_a3TG,
 RuntimeRep>))
                          @ (TYPE
                               (b_X444 |> <(type pat) k1_X440, RuntimeRep>)
                             -> *)
                          @ (->)
                          @ (b_X4hY |> <(type pat) k1_X4hU, TYPE
                                                              (b_a3TI |>
 Nth:2
 (Sym cobox_a3TS))>)
                          (Data.Typeable.Internal.TrTyCon
                             @ (TYPE (b_a3TI |> Nth:2 (Sym cobox_a3TS))
                                -> TYPE (b_X444 |> Nth:2 (Sym cobox_X44r))
                                -> *)
                             @ (->)
                             sc_s7Yr
                             sc_s7Ys
                             GHC.Types.$tc(->)
                             sc_s7Yt)
                          sc_s7Yv
              = $smkTrApp_s7Ze
                  @ k1_X4hU
                  @ b_X4hY
                  @ k1_X440
                  @ b_X444
                  @ k1_a3TG
                  @ b_a3TI
                  sc_s7Yv
                  @~ (cobox_X44r
                      :: (RuntimeRep -> * :: *) ~# (k1_X440 -> * :: *))
                  sc_s7Yr
                  sc_s7Ys
                  sc_s7Yt
                  @~ (cobox_a3TS
                      :: (RuntimeRep -> * :: *) ~# (k1_a3TG -> * :: *))]
 }}}
 This is no good in at least two ways
 * We mention `cobox_a3TS` in the kind of `sc_s7Yv`, but don't bind it
 until later in the telescope.
 * Matching against the LHS will not bind those `cobox` variables, because
 the type matcher discards casts (and rightly so).

 So that's  the problem.

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