2008/10/6 Jason Dagit
\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