Names still do matter where they shouldn't
nicolabotta opened this issue · 0 comments
nicolabotta commented
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.