Почему Idris связывает имя значения с именем аргумента типа, которое впоследствии определяется?

Question

Haskell позволяет:

a:: Int 
a = 3
data MyList a = Nil | Cons a (MyList a) 

В то время как Идрис будет жаловаться на a is bound as an implicit, и мне нужно использовать другой аргумент типа:

a: Int 
a = 3
data MyList b = Nil | Cons b (MyList b)

Answer 1

На самом деле, Идрис не связывает их здесь, потому что a в нижнем регистре. Но он может - кроме Haskell - потому что он поддерживает значения в типах. Таким образом, компилятор предупреждает вас, потому что это общий источник ошибок. Предположим, вы пишете:

n : Nat
n = 3

doNothing : Vect n Int -> Vect n Int
doNothing xs = xs

Вы можете ожидать, что тип doNothing - Vect 3 Int -> Vect 3 Int. Но вместо этого строчные аргументы должны быть неявными , а тип doNothing на самом деле {n : Nat} -> Vect n Int -> Vect n Int, несмотря на ранее объявленный n. Вы должны написать Vect Main.n Int или сделать N заглавными буквами, чтобы использовать его.

Таким образом, компилятор думает, что, возможно, вы хотели сделать что-то похожее с a в MyList a и предупреждает вас.