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.