Type inference depends on order of equality
The order of two types in an equality GADT controls whether a program is accepted:
{-# LANGUAGE TypeFamilyDependencies, PartialTypeSignatures #-}
module Scratch where
import Prelude (Int, String, undefined)
data Eq a b where
Refl :: Eq a a
type family Mt a = r | r -> a
anyM :: Mt a
anyM = undefined
useIntAndRaise :: Mt Int -> a
useIntAndRaise = undefined
type family Nt a = r | r -> a
use :: Nt a -> a
use = undefined
anyN :: Nt a
anyN = undefined
foo p (e :: Eq (Mt Int) (Nt String)) =
(case e of
Refl ->
let bar x =
if p then useIntAndRaise x
else use x
in
bar) anyM
As written, that is accepted. But if you change the type of e
to be Eq (Nt String) (Mt Int)
, then it is rejected (though also changing the final anyM
to anyN
makes it accepted again).
In general, I think it will be hard (read: impossible) to get this to work in all possible scenarios: the choice of which type we prefer between Mt Int
and Nt String
will leak out of the GADT match. So this probably isn't a bug in the implementation, but rather in the design.
This is not very important, but it was a curiosity that came up in conversation.