Typeable regression in GHC HEAD
I recently wrote some code while exploring a fix for #13327 that heavily uses poly-kinded 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/ghc-stage2 --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.