[GHC] #11334: GHC panic when calling typeOf on a promoted data constructor

[GHC]

#11334: GHC panic when calling typeOf on a promoted data constructor
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  bgamari
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  8.0.1-rc1
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash                              |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D1757
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by bgamari):

 **Disclaimer**: The following commentary is dangerously ignorant. I've
 glanced at a few papers and read a bit of code but otherwise have
 vanishingly little knowledge about the type checker.

 I'm looking at this slightly easier example (which still replicates the
 failure),

 {{{#!hs
 {-# LANGUAGE PolyKinds #-}

 module Other where

 data Other (f :: k -> *) (a :: k) = Other (f a)
 }}}

 {{{#!hs
 {-# LANGUAGE DataKinds #-}
 module Main where

 import Data.Typeable
 import Other

 main :: IO ()
 main = let a = typeOf (undefined :: Proxy 'Other) in return ()
 }}}

 As before enabling `PolyKinds` in `Main` results in the expected insoluble
 `Typeable` error.

 `-ddump-tc-trace -fprint-explicit-kinds` produces the following suspicious
 output,
 {{{
 decideKindGeneralisationPlan
   type: (Proxy k1_aJt[tau:5] ('Other k_aJB[tau:5] f_aJC[tau:5]
 a_aJD[tau:5] |> <f_aJC[tau:5] a_aJD[tau:5] -> Other k_aJB[tau:5]
 f_aJC[tau:5] a_aJD[tau:5]>_N) |> <*>_N)
   ftvs: [k1_aJt[tau:5], f_aJC[tau:5], a_aJD[tau:5], k_aJB[tau:5]]
   should gen? True
 writeMetaTyVar k_aJB[tau:5] :: * := *
 writeMetaTyVar f_aJC[tau:5] :: k_aJB[tau:5] -> * := *
 writeMetaTyVar a_aJD[tau:5] :: k_aJB[tau:5] := *
 }}}

 If I'm interpreting this correctly `f` (which is of kind `k -> *`) is
 being instantiated as `*`.

 I'm going to eat some food; more later.

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