[Haskell-cafe] Inferred type is less polymorphic than expected, depends on order

[Ryan Ingram]

2008/10/6 Jason Dagit <dagit at codersbase.com>:
> \begin{code}
> badOrder :: (Sealed (p x)) -> (forall b. (Sealed (q b))) -> (Sealed (q x))
> badOrder sx sy = case sy of
>                  Sealed y -> case sx of
>                              Sealed x -> Sealed (f x y)
> \end{code}
>
> \begin{code}
> goodOrder :: (Sealed (p x)) -> (forall b. (Sealed (q b))) -> (Sealed (q x))
> goodOrder sx sy = case sx of
>                   Sealed x -> case sy of
>                               Sealed y -> Sealed (f x y)
> \end{code}

It may help if you transform this a bit closer to System F with
existentials & datatypes:
/\ = forall
@t = type application, with the rule:

(a :: forall x. b) @t :: (replace occurrences of x in b with t)

-- the quantified type "x" gets packed into the data
-- and comes out when you pattern match on it
data Sealed s where
    Sealed :: /\t. s t -> Sealed s

goodOrder = \sx :: Sealed (p x) -> \sy :: (/\b. Sealed (q b)) ->
    case sx of (Sealed @y pxy) ->
        case (sy @y) of (Sealed @z qyz) ->
            Sealed @z (f pxy qyz)

badOrder = \sx :: Sealed (p x) -> \sy :: (/\b. Sealed (q b)) ->
    -- in order to pattern-match on sy, we need to give it a type
    -- so we just pick an arbitrary type "unknown" or "u" distinct
from any other type we know about
    case (sy @u) of (Sealed @z quz) ->
        case sx of (Sealed @y pxy) ->
            Sealed @z (f pxy quz) -- doesn't typecheck!

In the good order, you have already unpacked the existential for sx,
so you know what type to instantiate sy at.  In the bad order, you
don't know what type to instantiate sy at.

  -- ryan