Sorry I forgot to reply to the list Alex -------- Forwarded Message -------- Subject: Re: [Haskell-cafe] Strange "ambiguity" problems thanks to GADTs Date: Wed, 22 Jul 2015 13:24:56 +0100 From: Alexander Eyers-Taylor <aeyerstaylor11@gmail.com> To: Andres Loeh <mail@andres-loeh.de> Hi In this case what happens in the type checker is that after checking the start of the let we give the variable e1 a type (say abt0a) Then we enter the case. When entering the case, as SFun introduces a constaint (SFun is actually of type (a ~ Maybe j) => Sing a). As we have a constraint we cannot then unify the variables. The reason we can't unify is that we cant tell that (a ~ Maybe j) does not imply (abt0 ~ abt'). In GHC 6.12 the old type inference algotrithm was used. This had some problems as it didn't always infer a priciple type for GADTs. The new inference algorithm OutsideIn does this in a more principled way. In the non-indexed versions when we do the pattern match no constaints are introduced so we can typecheck as usual Alex On 22/07/15 07:59, Andres Loeh wrote:

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@gmail.com> wrote:

...

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

---

Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe