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

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 wrote:

On Wed, Jul 8, 2015 at 9:14 PM, Richard Eisenberg 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe