[Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour

[Alexis King]

What you say may be true, but the behavior you describe is still inconsistent with the documentation. After all, the documentation states these things must all be simultaneously true:

Scoped type variables stand for type variables, not arbitrary types.
Distinct scoped type variables correspond to distinct type variables.
The type variables are always rigid.

Tom’s program can’t possibly obey all three of these things because that would imply that `x :: a` and `y :: b` where `a` and `b` are distinct skolems, so `add` could not possibly typecheck. But it does—so it sounds like older versions of GHC just diverged from the documentation in other, less significant ways.

Alexis

> On Aug 19, 2020, at 14:53, Viktor Dukhovni <ietf-dane at dukhovni.org> wrote:
> 
> I added some follow up comments to the ticket you opened.  I don't agree
> with the analysis.  Best I can tell (with some confidence after also
> testing with GHC 8.0 which predates the above proposal), is that instead
> what's happening is:
> 
>    1.  The function has no explicit type signature, the below is
>        just a term-level formula for its value:
> 
>            add (x :: a) (y :: a) = x + y
> 
>    2.  The type signature is inferred as usual:
> 
>            add :: Num c => c -> c -> c
> 
>        unifying the type `c` with the types of both of the terms `x`
>        and `y`.
> 
>    3.  But the formula contains two Pattern Type Signatures, binding
>        the lexical type variable `a` to the type of `x` and the lexical
>        type variable `b` to the type of `y`.
> 
>    4.  However the types of `x` and `y` are both `c` (really some
>        arbitrary fixed type variable, modulo alpha-renaming).
> 
>    5.  Therefore, `a` and `b` are both the same type, not by virtue
>        of type inference between `a` and `b`, but by virtue of simple
>        pattern matching to an ultimately common type.
> 
> The only thing that changed after the proposal was broadening of the
> acceptable pattern matching to allow the pattern to match something
> other than a type *variable*:
> 
> Before:
> 
>    f :: a -> Int
>    f (x :: b) = 1      -- OK b ~ a
> 
>    f :: Int -> Int
>    f (x :: b) = 1      -- Bad b ~ Int, not a type variable!
> 
> After: 
> 
>    f :: a -> Int
>    f (x :: b) = 1      -- OK b ~ a
>    f :: Int -> Int
>    f (x :: b) = 1      -- OK b ~ Int
> 
> However, Tom's example works both with GHC 8.0.x -- 8.6.x which fall
> into the *before* case, and with GHC 8.8 and up, which are in the
> *after* case.
> 
> -- 
>    Viktor.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200819/1bbaf2a2/attachment.html>