On Wed, Jul 8, 2015 at 9:14 PM, Richard Eisenberg
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