Poor error message which masks occurs-check failure

Here's some code, reduced from an example in https://github.com/ekmett/constraints/issues/55:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

import Data.Proxy
import GHC.Exts (Constraint)
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)

data Dict :: Constraint -> * where
  Dict :: a => Dict a

infixr 9 :-
newtype a :- b = Sub (a => Dict b)

-- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@
(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r

newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))

magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o
magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))

type family Lcm :: Nat -> Nat -> Nat where

axiom :: forall a b. Dict (a ~ b)
axiom = unsafeCoerce (Dict :: Dict (a ~ a))

lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)
lcmNat = magic lcm

lcmIsIdempotent :: forall n. Dict (n ~ Lcm n n)
lcmIsIdempotent = axiom

newtype GF (n :: Nat) = GF Integer

instance KnownNat n => Num (GF n) where
  xf@(GF x) + GF y = GF $ (x+y) `mod` (natVal xf)
  xf@(GF x) - GF y = GF $ (x-y) `mod` (natVal xf)
  xf@(GF x) * GF y = GF $ (x*y) `mod` (natVal xf)
  abs = id
  signum xf@(GF x) | x==0 = xf
                   | otherwise = GF 1
  fromInteger = GF

x :: GF 5
x = GF 3

y :: GF 5
y = GF 4

foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n))

bar :: (KnownNat m)  => GF m -> GF m -> GF m
bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)

Compiling this (with either GHC 8.0.1, 8.0.2, 8.2.1, or HEAD) gives you a downright puzzling type error:

$ /opt/ghc/head/bin/ghci Bug.hs                  
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/  :? for help                      
Loaded GHCi configuration from /home/rgscott/.ghci                                        
[1 of 1] Compiling Main             ( Bug.hs, interpreted )                               
                                                                                          
Bug.hs:63:21: error:                                                                      
    • Couldn't match type ‘m’ with ‘Lcm m m’                                              
      ‘m’ is a rigid type variable bound by                                               
        the type signature for:                                                           
          bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m                    
        at Bug.hs:62:1-44                                                                 
      Expected type: GF m                                                                 
        Actual type: GF (Lcm m m)                                                         
    • In the first argument of ‘(-)’, namely ‘foo x y’                                    
      In the expression:                                                                  
        foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)                 
      In an equation for ‘bar’:                                                           
          bar (x :: GF m) y
            = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
    • Relevant bindings include
        y :: GF m (bound at Bug.hs:63:17)
        x :: GF m (bound at Bug.hs:63:6)
        bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
   |
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
   |                     ^^^^^^^

Bug.hs:63:31: error:
    • Could not deduce: m ~ Lcm m m
      from the context: m ~ Lcm m m
        bound by a type expected by the context:
                   m ~ Lcm m m => GF m
        at Bug.hs:63:31-85
      ‘m’ is a rigid type variable bound by
        the type signature for:
          bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
        at Bug.hs:62:1-44
      Expected type: GF m
        Actual type: GF (Lcm m m)
    • In the first argument of ‘(\\)’, namely ‘foo y x’
      In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
      In the second argument of ‘(-)’, namely
        ‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
    • Relevant bindings include
        y :: GF m (bound at Bug.hs:63:17)
        x :: GF m (bound at Bug.hs:63:6)
        bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
   |
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
   |                               ^^^^^^^

In particular, I'd like to emphasize this part:

    • Could not deduce: m ~ Lcm m m
      from the context: m ~ Lcm m m

Wat!? Surely, GHC can deduce m ~ Lcm m m from m ~ Lcm m m? I decided to flip on -fprint-explicit-kinds and see if there was some other issue lurking beneath the surface:

$ /opt/ghc/head/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.3.20170509: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main             ( Bug.hs, interpreted )

Bug.hs:63:21: error:
    • Couldn't match type ‘m’ with ‘Lcm m m’
      ‘m’ is a rigid type variable bound by
        the type signature for:
          bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
        at Bug.hs:62:1-44
      Expected type: GF m
        Actual type: GF (Lcm m m)
    • In the first argument of ‘(-)’, namely ‘foo x y’
      In the expression:
        foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
      In an equation for ‘bar’:
          bar (x :: GF m) y
            = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
    • Relevant bindings include
        y :: GF m (bound at Bug.hs:63:17)
        x :: GF m (bound at Bug.hs:63:6)
        bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
   |
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
   |                     ^^^^^^^

Bug.hs:63:31: error:
    • Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
      from the context: m ~ Lcm m m
        bound by a type expected by the context:
                   m ~ Lcm m m => GF m
        at Bug.hs:63:31-85
      ‘m’ is a rigid type variable bound by
        the type signature for:
          bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
        at Bug.hs:62:1-44
      Expected type: GF m
        Actual type: GF (Lcm m m)
    • In the first argument of ‘(\\)’, namely ‘foo y x’
      In the first argument of ‘(\\)’, namely ‘foo y x \\ lcmNat @m @m’
      In the second argument of ‘(-)’, namely
        ‘foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)’
    • Relevant bindings include
        y :: GF m (bound at Bug.hs:63:17)
        x :: GF m (bound at Bug.hs:63:6)
        bar :: GF m -> GF m -> GF m (bound at Bug.hs:63:1)
   |
63 | bar (x :: GF m) y = foo x y - foo y x \\ lcmNat @m @m \\ Sub @() (lcmIsIdempotent @m)
   |

Well, not a whole lot changed. We now have this, slightly more specific error instead:

    • Could not deduce: (m :: Nat) ~~ (Lcm m m :: Nat)
      from the context: m ~ Lcm m m

Huh, this is flummoxing. Surely (m :: Nat) ~~ (Lcm m m :: Nat) ought to be the same thing as m ~ Lcm m m, right?