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

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. Richard On Jul 7, 2015, at 12:05 PM, 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