Wrong location reported for kind error

When I try to compile

{-# LANGUAGE PolyKinds, ConstraintKinds, TypeFamilies, FlexibleContexts #-}

module Bug where

import Data.Proxy

type T (a :: k1) (b :: k2) = (a ~ b, Show (Proxy (a :: k1)), Show (Proxy (b :: k2)))

I get

Bug.hs:7:80: error:
    • Couldn't match ‘k1’ with ‘k2’
    • In the type declaration for ‘T’
  |
7 | type T (a :: k1) (b :: k2) = (a ~ b, Show (Proxy (a :: k1)), Show (Proxy (b :: k2)))
  |                                                                                ^^

The problem is that the k2 that's highlighted has nothing at all to do with the error. Indeed, some experimentation shows that GHC will highlight the first occurrence of k2 to the right of the =. The error is actually from unification caused by a ~ b.

I noticed this because I've been tightening up the way GHC does left-to-right ordering during implicit quantification (while working on something more substantial). In so doing, I made sure to prefer kind variable occurrences to the left of the = over those to the right. But then I got a testsuite failure due to a changed location of an error.

This is caused by the call to report_sig_tv_err in tcTyClTyVars.

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture