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

[Oleg Grenrus]

Nailing down `abt` and `abt’`, but keeping `a` free makes the trick:

    {-# LANGUAGE DataKinds, PolyKinds, GADTs, RankNTypes, ScopedTypeVariables #-}

    data Type = Fun Type Type | Unit

    data Sing :: Type -> * where
       SUnit :: Sing Unit
       SFun  :: Sing i -> Sing j -> Sing (Fun i j)

    data AST :: (Type -> *) -> Type -> * where
       TT :: AST ast Unit
       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

    type TypeCheckMonad = Maybe

    inferType
       :: forall abt abt' a. (ABT abt, WellTypedABT abt')
       => abt a
       -> TypeCheckMonad (abt' a)
    inferType e0 = go e0
      -- b is free, abt and abt' are bounded, class dictionaries come from above.
      where go :: forall b. abt b -> TypeCheckMonad (abt' b)
            go e0' = case view e0' of
                       TT -> return . unviewWT SUnit $ TT
                       App e1 e2 -> do
                       e1' <- go e1
                       case typeOf e1' of
                         -- -Wall doesn't warn about missing SUnit case here, victory!
                         SFun _typ2 typ3 -> do
                           e2' <- inferType e2
                           return . unviewWT typ3 $ App e1' e2'

> On 07 Jul 2015, at 19:05, 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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150722/f66b9c37/attachment.sig>