Idris Type mismatch that occurs even from template

Question

Testing out an "easy" example of identity types, mod equality, but transitivity proof wont type check, even from the template. More than a fix, I want to know why?

Here's a snippet of the minimal problem

data ModEq : (n:Nat) -> (x:Nat) -> (y:Nat) -> Type where
    {- 3 constructors
        reflexive:      x == x (mod n), 
        left-induct:    x == y (mod n) => (x+n) == y    (mod n)
        right-induct:   x == y (mod n) => x == (y+n)    (mod n)
    -}
  Reflex : (x:Nat) -> ModEq n x x  --- Needs syntatic sugar, for now prefix
  LInd : (ModEq n x y) -> ModEq n (x+n) y
  RInd : (ModEq n x y) -> ModEq n x (y+n)

{----- Proof of transitive property. -----}
total
isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
{- x=x & x=y => x=y -}
isTrans (Reflex x) v = v
isTrans u (Reflex y) = u
{- ((x=y=>(x+n)=y) & y=z) => x=y & y=z => x=z (induct) => (x+n)=z -}
isTrans (LInd u) v = LInd (isTrans u v)
isTrans u (RInd v) = RInd (isTrans u v)
{- (x=y=>x=(y+n)) & (y=z=>(y+n)=z) => x=y & y=z => x=z (induct) -}
isTrans (RInd u) (LInd v) = isTrans u v

The type mismatch is in the last line, even though from the comment line I really cannot tell why logically its wrong. Here's the error:

48 | isTrans (RInd u) (LInd v) = isTrans u v
   | ~~~~~~~
When checking left hand side of isTrans:
When checking an application of Main.isTrans:
        Type mismatch between
                ModEq n (x + n) z (Type of LInd v)
        and
                ModEq n (y + n) z (Expected type)

        Specifically:
                Type mismatch between
                        plus x n
                and
                        plus y n

Not only am I confused by how LInd v got assigned the (wrong seeming) type ModEq n (x+n) z, but I point out that when I simply try the "type-define-refine" approach with the built in template I get:

isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
isTrans (RInd _) (LInd _) = ?isTrans_rhs_1

And even this wont type-check, it complains:

40 | isTrans (RInd _) (LInd _) = ?isTrans_rhs_1
   | ~~~~~~~
When checking left hand side of isTrans:
When checking an application of Main.isTrans:
        Type mismatch between
                ModEq n (x + n) z (Type of LInd _)
        and
                ModEq n (y + n) z (Expected type)

        Specifically:
                Type mismatch between
                        plus x n
                and
                        plus y n

Answer 1

The issue is that the compiler isn't able to deduce in your last case that y = {x + n}. You can give it this hint, though:

isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
isTrans (Reflex _) v = v
isTrans u (Reflex _) = u
isTrans (LInd u) v = LInd $ isTrans u v
isTrans u (RInd v) = RInd $ isTrans u v
isTrans (RInd u) (LInd v) {n} {x} {y = x + n} = ?isTrans_rhs

Which gives you the following goal for isTrans_rhs:

  x : Nat
  n : Nat
  u : ModEq n x x
  z : Nat
  v : ModEq n x z
--------------------------------------
isTrans_rhs : ModEq n x z

and thus, you can conclude with isTrans (RInd u) (LInd v) {n} {x} {y = x + n} = v