Typeable regression in GHC HEAD
I recently wrote some code while exploring a fix for #13327 that heavily uses polykinded Typeable
. This compiles without issue on GHC 8.0.1 and 8.0.2:
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE GADTs #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeInType #}
{# LANGUAGE TypeOperators #}
module DataCast where
import Data.Data
import GHC.Exts (Constraint)
data T (phantom :: k) = T
data D (p :: k > Constraint) (x :: j) where
D :: forall (p :: k > Constraint) (x :: k). p x => D p x
class Possibly p x where
possibly :: proxy1 p > proxy2 x > Maybe (D p x)
dataCast1T :: forall k c t (phantom :: k).
(Typeable k, Typeable t, Typeable phantom, Possibly Data phantom)
=> (forall d. Data d => c (t d))
> Maybe (c (T phantom))
dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing > Nothing
Just D > gcast1 f
But on GHC HEAD, it barfs this error:
$ ~/Software/ghc2/inplace/bin/ghcstage2 interactive Bug.hs
GHCi, version 8.1.20170223: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling DataCast ( Bug.hs, interpreted )
Bug.hs:28:29: error:
• Could not deduce (Typeable T) arising from a use of ‘gcast1’
GHC can't yet do polykinded Typeable (T :: * > *)
from the context: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom)
bound by the type signature for:
dataCast1T :: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom) =>
(forall d. Data d => c (t d)) > Maybe (c (T phantom))
at Bug.hs:(22,1)(25,35)
or from: (k ~ *, (phantom :: k) ~~ (x :: *), Data x)
bound by a pattern with constructor:
D :: forall k (p :: k > Constraint) (x :: k). p x => D p x,
in a case alternative
at Bug.hs:28:23
• In the expression: gcast1 f
In a case alternative: Just D > gcast1 f
In the expression:
case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing > Nothing
Just D > gcast1 f

28  Just D > gcast1 f
 ^^^^^^^^
That error message itself is hilariously strange, since GHC certainly has the power to do polykinded Typeable
nowadays.
Marking as high priority since this is a regression—feel free to lower the priority if you disagree.