Skip to content

GitLab

Closed
Opened by Krzysztof Gogolewski@monoidalDeveloper

Linear types: implicit quantification in GADTs

The following code is mistakenly rejected:

data Existential a where
  MkE :: a %p -> Existential a
Not in scope: type variable ‘p’

This is because the renamer doesn't look at multiplicities of fields when computing implicitly bound variables. This isn't very important because it doesn't make much sense to have existential multiplicities, but it's a clear bug.

Edited by Krzysztof Gogolewski