<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=windows-1252">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<br>
<div class="moz-forward-container">Sorry I forgot to reply to the
list<br>
<br>
Alex<br>
<br>
-------- Forwarded Message --------
<table class="moz-email-headers-table" border="0" cellpadding="0"
cellspacing="0">
<tbody>
<tr>
<th valign="BASELINE" nowrap="nowrap" align="RIGHT">Subject:
</th>
<td>Re: [Haskell-cafe] Strange "ambiguity" problems thanks
to GADTs</td>
</tr>
<tr>
<th valign="BASELINE" nowrap="nowrap" align="RIGHT">Date: </th>
<td>Wed, 22 Jul 2015 13:24:56 +0100</td>
</tr>
<tr>
<th valign="BASELINE" nowrap="nowrap" align="RIGHT">From: </th>
<td>Alexander Eyers-Taylor <a class="moz-txt-link-rfc2396E" href="mailto:aeyerstaylor11@gmail.com"><aeyerstaylor11@gmail.com></a></td>
</tr>
<tr>
<th valign="BASELINE" nowrap="nowrap" align="RIGHT">To: </th>
<td>Andres Loeh <a class="moz-txt-link-rfc2396E" href="mailto:mail@andres-loeh.de"><mail@andres-loeh.de></a></td>
</tr>
</tbody>
</table>
<br>
<br>
<pre>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 <a class="moz-txt-link-rfc2396E" href="mailto:winterkoninkje@gmail.com"><winterkoninkje@gmail.com></a> wrote:
>> On Wed, Jul 8, 2015 at 9:14 PM, Richard Eisenberg <a class="moz-txt-link-rfc2396E" href="mailto:eir@cis.upenn.edu"><eir@cis.upenn.edu></a> 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
>> <a class="moz-txt-link-abbreviated" href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a>
>> <a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a>
> _______________________________________________
> Haskell-Cafe mailing list
> <a class="moz-txt-link-abbreviated" href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a>
> <a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a>
</pre>
<br>
</div>
<br>
</body>
</html>