[Haskell-cafe] Counterintuitive ScopedTypeVariables behaviour
Tom Ellis
tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk
Sun Aug 16 12:17:11 UTC 2020
I have just noticed that with ScopedTypeVariables one can write the
following bizarre definition
-- Inferred signature:
-- add :: Num a => a -> a -> a
add (x :: a) (y :: b) = x + y
The reason for this behaviour is that
> in all patterns other than pattern bindings, a pattern type
> signature may mention a type variable that is not in scope; in this
> case, the signature brings that type variable into scope.
https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#pattern-type-signatures
and the justification is that
> Bringing type variables into scope is particularly important for
> existential data constructors
But this leads to a rather puzzling user experience. Was it really
not possible to design this extension in a way that would allow
bringing new type variables into scope locally but not allow them to
unify with other type variables from outer scopes?
To be more concrete, what I would like to see is a design where `k` is
allowed because the type `a` (bound within a pattern) does not need to
unify with anything but `k2` is not allowed because `a` is forbidden
to unify with `b`. `k3` would also be forbidden (the type variables
called `a` are actually distinct) as would `k4` (the type variable for
the inferred signature would be fresh and distinct from `a`).
I believe this design might lead to much less puzzling behaviour.
Would it be possible (within a new extension, of course) or have I
overlooked something?
Tom
data T = forall a. MkT [a]
k :: T -> T
k (MkT [t::a]) =
MkT t3
where
(t3::[a]) = [t,t,t]
data T2 a = MkT2 [a]
k2 :: T2 b -> T2 b
k2 (MkT2 [t::a]) =
MkT2 t3
where
(t3::[a]) = [t,t,t]
k3 :: T2 a -> T2 a
k3 (MkT2 [t::a]) =
MkT2 t3
where
(t3::[a]) = [t,t,t]
k4 (MkT2 [t::a]) =
MkT2 t3
where
(t3::[a]) = [t,t,t]
More information about the Haskell-Cafe
mailing list