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

[Alexander Eyers-Taylor]

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



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20150722/acc7dc78/attachment.html>