Hi. I've drastically reduced the example. This program triggers the same error:

{-# LANGUAGE GADTs, KindSignatures #-}

data Sing :: * -> * where SFun :: Sing (Maybe j)

class WellTypedABT (abt :: * -> *) where typeOf :: abt a -> Sing a

inferType :: (WellTypedABT abt') => abt a -> abt' a inferType e1 = let e1' = inferType e1 in case typeOf e1' of SFun -> e1'

Btw, this compiles fine with ghc-6.12 (as does a version of the original program if we replace the data kinds involved by equivalent kind-*-datatypes). Cheers, Andres On Wed, Jul 22, 2015 at 1:11 AM, wren romano wrote:

On Wed, Jul 8, 2015 at 9:14 PM, Richard Eisenberg wrote:

...

I think GADTs are a red herring here -- this is the classic show/read ambiguity dressed up. In the code below, how should GHC determine the type of e1' or e2'? There's no way to know.

Except that when I erase the indices, everything works just fine:

{-# LANGUAGE KindSignatures, GADTs #-}

data Type = Fun Type Type

data AST :: * -> * where App :: ast -> ast -> AST ast

class ABT (abt :: *) where view :: abt -> AST abt unview :: AST abt -> abt

class WellTypedABT (abt :: *) where unviewWT :: Type -> AST abt -> abt typeOf :: abt -> Type

data TypeCheckMonad a = TCM { unTCM :: a }

instance Functor TypeCheckMonad where fmap f = TCM . f . unTCM

instance Applicative TypeCheckMonad where pure = TCM TCM f <*> TCM x = TCM (f x)

instance Monad TypeCheckMonad where return = pure TCM x >>= k = k x

inferType :: (ABT abt, WellTypedABT abt') => abt -> TypeCheckMonad abt' inferType e0 = case view e0 of App e1 e2 -> do e1' <- inferType e1 case typeOf e1' of Fun typ2 typ3 -> do e2' <- inferType e2 return . unviewWT typ3 $ App e1' e2'

-- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

I take back my claim that this is the show/read ambiguity. Alex's recent explanation looks spot on to me. Richard On Jul 22, 2015, at 3:53 AM, Oleg Grenrus wrote:

Nailing down `abt` and `abt’`, but keeping `a` free makes the trick:

{-# LANGUAGE DataKinds, PolyKinds, GADTs, RankNTypes, ScopedTypeVariables #-}

data Type = Fun Type Type | Unit

data Sing :: Type -> * where SUnit :: Sing Unit SFun :: Sing i -> Sing j -> Sing (Fun i j)

data AST :: (Type -> *) -> Type -> * where TT :: AST ast Unit App :: ast (Fun a b) -> ast a -> AST ast b

class ABT (abt :: Type -> *) where view :: abt a -> AST abt a unview :: AST abt a -> abt a

class WellTypedABT (abt :: Type -> *) where unviewWT :: Sing a -> AST abt a -> abt a typeOf :: abt a -> Sing a

type TypeCheckMonad = Maybe

inferType :: forall abt abt' a. (ABT abt, WellTypedABT abt') => abt a -> TypeCheckMonad (abt' a) inferType e0 = go e0 -- b is free, abt and abt' are bounded, class dictionaries come from above. where go :: forall b. abt b -> TypeCheckMonad (abt' b) go e0' = case view e0' of TT -> return . unviewWT SUnit $ TT App e1 e2 -> do e1' <- go e1 case typeOf e1' of -- -Wall doesn't warn about missing SUnit case here, victory! SFun _typ2 typ3 -> do e2' <- inferType e2 return . unviewWT typ3 $ App e1' e2'

...

On 07 Jul 2015, at 19:05, wren romano wrote:

On Tue, Jul 7, 2015 at 3:35 AM, Simon Peyton Jones wrote:

...

If you post a repro case someone (even me) might help. The devil is always in the details.

The smallest repro I can come up with (which is still related to the actual problem) is as follows. In case it matters for the solution, there are a number of important bits I've erased. Most importantly, the inferType function is actually mutually recursive with a checkType function, though that doesn't seem to be the cause of the problem.

{-# LANGUAGE DataKinds, PolyKinds, GADTs #-}

data Type = Fun Type Type

data Sing :: Type -> * where SFun :: Sing i -> Sing j -> Sing (Fun i j)

data AST :: (Type -> *) -> Type -> * where App :: ast (Fun a b) -> ast a -> AST ast b

class ABT (abt :: Type -> *) where view :: abt a -> AST abt a unview :: AST abt a -> abt a

class WellTypedABT (abt :: Type -> *) where unviewWT :: Sing a -> AST abt a -> abt a typeOf :: abt a -> Sing a

data TypeCheckMonad a = TCM { unTCM :: a }

instance Functor TypeCheckMonad where fmap f = TCM . f . unTCM

instance Applicative TypeCheckMonad where pure = TCM TCM f <*> TCM x = TCM (f x)

instance Monad TypeCheckMonad where return = pure TCM x >>= k = k x

inferType :: (ABT abt, WellTypedABT abt') => abt a -> TypeCheckMonad (abt' a) inferType e0 = case view e0 of App e1 e2 -> do e1' <- inferType e1 case typeOf e1' of SFun typ2 typ3 -> do e2' <- inferType e2 return . unviewWT typ3 $ App e1' e2' -- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe