Richard Eisenberg eir at cis.upenn.edu
Thu Jul 9 01:14:41 UTC 2015

```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 }
>
>    fmap f = TCM . f . unTCM
>
>    pure = TCM
>    TCM f <*> TCM x = TCM (f x)
>
>    return      = pure
>    TCM x >>= k = k x
>
> inferType
>    :: (ABT abt, WellTypedABT abt')
>    => 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
> _______________________________________________