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

[Richard Eisenberg]

I take back my claim that this is the show/read ambiguity. Alex's recent explanation looks spot on to me.

Richard

On Jul 22, 2015, at 3:53 AM, Oleg Grenrus <oleg.grenrus at iki.fi> wrote:

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