Issue261.agda

module Issue261 where

postulate
  List : Set → Set
  nil : ∀ A → List A
  Nat : Set

works-now : List Nat
works-now with nil _
... | xs = xs