Why does Idris conflate a value name with a type argument name that is subsequently defined?

Question

Haskell allows:

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

Whereas Idris will complain with a is bound as an implicit, and I need to use a different type argument:

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

xash xash · Accepted Answer · 2018-05-07T06:08:05

Actually, Idris does not conflate them here, because a is lower case. But it could – other than Haskell – because it supports values in types. So the compiler warns you, because that is a common source for errors. Suppose you write:

n : Nat
n = 3

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

You might expect that doNothing's type is Vect 3 Int -> Vect 3 Int. But instead lower case arguments are bound to be implicit and doNothing's type is actually {n : Nat} -> Vect n Int -> Vect n Int, despite the previous declared n. You'd have to write Vect Main.n Int or make N upper case to use it.

So the compiler thinks that maybe you wanted to do something similiar with the a in MyList a and warns you.

Why does Idris conflate a value name with a type argument name that is subsequently defined?

1 Answers