Brian Hulley wrote:
Ross Paterson wrote:
data T = forall a. MkT [a]
k :: T -> T k (forall a. MkT [t]) = MkT t3 where t3::[a] = [t,t,t]
What was wrong with the example in the documentation?
k :: T -> T k (MkT [t::a]) = MkT t3 where t3::[a] = [t,t,t]
The type of (t) is (a) - what could possibly be simpler?
No doubt I'm missing something because the docs then go on to say "If this seems a little odd..." - but it doesn't. It makes perfect sense. Why shouldn't a pattern type signature introduce a scoped type variable? It also has the advantage that you can see what the type variable is supposed to represent without having to track down the original data declaration.
If the problem is that pattern type signatures normally have an implicit forall (which stops them introducing lexically scoped type variables), perhaps the implicit forall could be discarded so that any type variables in a pattern signature not in the scope of an *explicit* forall would be lexically scoped over the whole of an equation (or the guarded part if they occur first in the guard) eg: foo (f :: a -> b) (x:: a) = ((f x) :: b) meaning: forall a b. (foo (f :: a -> b) (x :: a) = ((f x) :: b)) and foo (f :: forall a. a-> b) x = ((f x) :: b) meaning: forall b. (foo (f :: forall a. a-> b) x = ((f x) :: b)) Apologies if I'm still missing what the real problem is, Brian.