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

[wren romano]

Hi all,

In my latest project I've been using a bunch of GADTs, which
unfortunately disables let-polymorphism (i.e., where-polymorphism) in
the most annoying way. For the most part I've been able to hack around
that limitation via judicious use of ScopedTypeVariables, but I've run
into an issue that I can't for the life of me figure out why GHC
doesn't like it.

I have something like the following function, where @a@ and @b@ happen
to be GADTs:

foo :: (A a, B b) => a i -> M (b i)
foo a =
case view a of
...
SomePattern a1 a2 -> do
b1 <- foo a1
b2 <- foo a2
return . unview $ SomePattern b1 b2

It seems to me that the recursive calls should work just fine, using
the same @b@ as we'll ultimately be returning. However, for some
reason GHC complains about the recursive calls using some other @b0@
can can't deduce @B b0@ from @B b@. Why doesn't GHC unify these two
types? How can I force them to unify without adding type annotations
at every recursive call?

--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

[Marco Vassena]

Hi Wren,

I think that the ambiguity comes from the fact

that the type variable b is mentioned only 

in the constraints and in the result type.

Crucially the instance B b selected determines the result b,

and this in general leads to ambiguity because instances

are chosen automatically behind the scenes.

A standard way to fix this is to include the ambiguous type b

among the types of the arguments.

With this trick it is possible to drive the instance choice to select

the correct one passing the right argument, avoiding any ambiguity.

For example you can use a Proxy b [1], to force the recursive

calls to reuse the same b. 

   foo :: (A a, B b) => a i -> Proxy b -> M (b i)
   foo a p =

       case view a of
       ...
       SomePattern a1 a2 -> do

           b1 <- foo p a1
           b2 <- foo p a2

           return . unview $ SomePattern b1 b2

I hope this helps.

All the best,

Marco

[1] https://hackage.haskell.org/package/base-4.7.0.2/docs/Data-Proxy.html

[wren romano]

On Tue, Jul 7, 2015 at 3:35 AM, Simon Peyton Jones
<sim...@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'

[Richard Eisenberg]

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.

Richard

[wren romano]

On Wed, Jul 8, 2015 at 9:14 PM, Richard Eisenberg <e...@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

[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

[Oleg Grenrus]

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'

[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 <aeyerst...@gmail.com>
To:	Andres Loeh <ma...@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 <winterk...@gmail.com> wrote:
>> On Wed, Jul 8, 2015 at 9:14 PM, Richard Eisenberg <e...@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
>> Haskel...@haskell.org

[Richard Eisenberg]

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

Richard