[GHC] #14845: TypeInType, index GADT by constraint witness

[GHC]

#14845: TypeInType, index GADT by constraint witness
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.5
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #13895            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 This is the test case from #13895:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeInType #-}
 module Foo where

 import Data.Data (Data, Typeable)
 import Data.Kind

 dataCast1 :: forall (a :: Type).
              Data a
           => forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable
 k => k -> Type).
              Typeable t
           => (forall d. Data d => c (t d))
           -> Maybe (c a)
 dataCast1 _ = undefined
 }}}

 {{{
 $ /opt/ghc/8.4.1/bin/ghci Bug.hs
 GHCi, version 8.4.0.20180224: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Foo              ( Bug.hs, interpreted )

 Bug.hs:11:23: error:
     • Illegal constraint in a type: Typeable k0
     • In the first argument of ‘Typeable’, namely ‘t’
       In the type signature:
         dataCast1 :: forall (a :: Type).
                      Data a =>
                      forall (c :: Type -> Type)
                             (t :: forall (k :: Type). Typeable k => k ->
 Type).
                      Typeable t => (forall d. Data d => c (t d)) -> Maybe
 (c a)
    |
 11 |              Typeable t
    |                       ^

 Bug.hs:12:38: error:
     • Illegal constraint in a type: Typeable k0
     • In the first argument of ‘c’, namely ‘(t d)’
       In the type signature:
         dataCast1 :: forall (a :: Type).
                      Data a =>
                      forall (c :: Type -> Type)
                             (t :: forall (k :: Type). Typeable k => k ->
 Type).
                      Typeable t => (forall d. Data d => c (t d)) -> Maybe
 (c a)
    |
 12 |           => (forall d. Data d => c (t d))
    |                                      ^^^
 }}}

 Note that there are no promoted constructors in this program! But changing
 the error message as per the suggestion in comment:9 means that the new
 error message for this program would (incorrectly) be:

 {{{
 Data constructor has a constraint `Typeable k0`, and thus cannot be
 promoted
 }}}

 Since the
 [http://git.haskell.org/ghc.git/blob/ffdb110a7f71b29f30adab7fea794b9f070a8e75:/compiler/typecheck/Inst.hs#l451
 place where this error message arises], `tcInstBinder`, has no knowledge
 of where the constraint comes from (in particular, whether it comes from a
 promoted constructor or not).

 I just want to make sure that if we do change this error message, that we
 don't degrade the quality of the error message in this program. But I have
 no idea how `tcInstBinder` works, so knowing how to propagate the relevant
 information down into `tcInstBinder` to make it aware of the provenance of
 the error message is far above my pay grade.

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