Dear all, Vlad has submitted a bug fix amendment to #448, to fix the wording around type variables in signatures within explicit type annotations: https://github.com/ghc-proposals/ghc-proposals/pull/556/files I’m shepherding that one myself. The gist is that in data Proxy a = P g :: Proxy (Nothing @(a, a)) -> () g (P @(Nothing :: Maybe (x, x))) = () the multiple occurrences of `a` are non-linear patterns and disallowed, but the multiple patterns of `x` are fine, because that’s how type variables in signatures in patterns happen to work. Vlad fixed the wording with regard to that in #448. Simon and Richard already signaled support on the Github thread, which I recommend to follow. I don’t expect much further discussion around this and will happily merge after a week of silence (or after one or two additional confirmations). Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/