[Haskell-cafe] Strange "ambiguity" problems thanks to GADTs

[wren romano]

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