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

[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.

Richard

On Jul 7, 2015, at 12:05 PM, wren romano <winterkoninkje at gmail.com> wrote:

> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe