Skip to content

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.

Edited by Ryan Scott
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information