Confusion of value-kinded type variables

[pieter-bos]

(In reference to #2572) I believe this example should be accepted by LH, but isn't:

{-# LANGUAGE TypeApplications #-}
module M where

import GHC.Num.Natural
{-@ embed GHC.Num.Natural.Natural as Int @-}

import GHC.TypeNats
import Data.Proxy

{-@ addByProxy :: forall x y . _ -> _ -> {v:_|v == x} -> {v:_|v == y} -> {v:_|v == x + y} @-}
addByProxy :: forall (x :: Nat) (y :: Nat) . Proxy x -> Proxy y -> Int -> Int -> Int
addByProxy _ _ x y = x + y

{-@ addByProxy' :: forall y x . _ -> _ -> {v:_|v == y} -> {v:_|v == x} -> {v:_|v == x + y} @-}
addByProxy' :: forall (y :: Nat) (x :: Nat) . Proxy y -> Proxy x -> Int -> Int -> Int
addByProxy' _ _ y x = addByProxy @y @x Proxy Proxy y x

My interpretation is that addByProxy @y roughly gets the type:

forall y . _ -> _ -> {v:_|v == y} -> {v:_|v == y} -> {v:_|v == y + y}

With no longer a way to distinguish the y local to addByProxy' and the y declared at the type signature of addByProxy. The errors are reported as follows:

Type Mismatch
.
The inferred type
  VV : {v : GHC.Types.Int | v == x + x}
.
is not a subtype of the required type
  VV : {VV##787 : GHC.Types.Int | VV##787 == x + y}
.
in the context
  x : GHC.Num.Natural.Natural
   
  y : GHC.Num.Natural.Natural

Type Mismatch
.
The inferred type
  VV : {v : GHC.Types.Int | v == y}
.
is not a subtype of the required type
  VV : {VV##791 : GHC.Types.Int | VV##791 == x}
.
in the context
  x : GHC.Num.Natural.Natural
   
  y : GHC.Num.Natural.Natural

[facundominguez]

Thanks for the report. It is telling that renaming y to z in the type of addByProxy' makes verification pass.