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

[Andres Loeh]

Hi.

I've drastically reduced the example. This program triggers the same error:

> {-# LANGUAGE GADTs, KindSignatures #-}
>
> data Sing :: * -> * where
>   SFun :: Sing (Maybe j)
>
> class WellTypedABT (abt :: * -> *) where
>   typeOf :: abt a -> Sing a
>
> inferType :: (WellTypedABT abt') => abt a -> abt' a
> inferType e1 =
>   let e1' = inferType e1
>   in  case typeOf e1' of
>         SFun -> e1'

Btw, this compiles fine with ghc-6.12 (as does a version of the
original program if we replace the data kinds involved by equivalent
kind-*-datatypes).

Cheers,
  Andres

On Wed, Jul 22, 2015 at 1:11 AM, wren romano <winterkoninkje at gmail.com> wrote:
> On Wed, Jul 8, 2015 at 9:14 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>> 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.
>
> Except that when I erase the indices, everything works just fine:
>
>
> {-# LANGUAGE KindSignatures, GADTs #-}
>
> data Type = Fun Type Type
>
> data AST :: * -> * where
>     App :: ast -> ast -> AST ast
>
> class ABT (abt :: *) where
>     view   :: abt -> AST abt
>     unview :: AST abt -> abt
>
> class WellTypedABT (abt :: *) where
>     unviewWT :: Type -> AST abt -> abt
>     typeOf   :: abt -> Type
>
> 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
>     -> TypeCheckMonad abt'
> inferType e0 =
>     case view e0 of
>     App e1 e2 -> do
>         e1' <- inferType e1
>         case typeOf e1' of
>             Fun 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