Names still do matter where they shouldn't

[nicolabotta]

The program

> %default total
> %access public export
> %auto_implicits off

> interface Functor F => VeriFunctor (F : Type -> Type) where
> 
>   mapPresId    : {X : Type} -> (fx : F X) -> map id fx = id fx
>   
>   mapPresComp  : {X, Y, Z : Type} -> (f : X -> Y) -> (g : Y -> Z) -> 
>                  (fx : F X) -> map (g . f) fx = (map g . map f) fx

fails to type check with idris --allow-capitalized-pattern-variables:

NamesDoMatter.lidr:5:13-55:
  |
5 | > interface Functor F => VeriFunctor (F : Type -> Type) where
  |             ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking left hand side of Main.mapPresComp:
When checking argument Z to Main.mapPresComp:
        Type mismatch between
                Nat (Type of 0)
        and
                Type (Expected type)

But replacing X, Y and Z with A, B and C makes the program type check fine.