Terrible error message from ->/~> confusion

[goldfirere]

Given

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}

module TypeMap where

import Unsafe.Coerce
import Data.Type.Equality
import Data.Proxy
-- import Data.Constraint

data TMap (key :: *) (v :: *)
type family (!!) :: TMap k v -> k -> Maybe v
leftBiasedUnion :: ((m !! k) :~: Just v)
                -> () -- ((Union m n !! k) :~: Just v)
leftBiasedUnion Refl = undefined -- unsafeCoerce Refl

we get

    Couldn't match representation of kind ‘TMap k v’ with that of ‘*’
    Inaccessible code in
      a pattern with constructor
        Refl :: forall k (a :: k). (:~:) k a a,
      in an equation for ‘leftBiasedUnion’
    Relevant bindings include
      leftBiasedUnion :: (:~:) (Maybe v) ((!!) k v m k1) ('Just v v1)
                         -> ()
        (bound at TypeMap.hs:40:1)
    In the pattern: Refl
    In an equation for ‘leftBiasedUnion’:
        leftBiasedUnion Refl = undefined

This is correct. But it arises from the fact that we're comparing TMap k v -> k -> Maybe v (the kind of !!) against forall a. a -> Maybe a (the kind of Just). Gross.

[goldfirere]

This problem also means that GHC is decomposing an arrow in one type and a forall in the other. Is that good? Probably not.