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

[wren romano]

On Tue, Jul 7, 2015 at 3:35 AM, Simon Peyton Jones
<simonpj at microsoft.com> 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