Implement visible dependent quantification
GHC proposal 35 (A syntax for visible dependent quantification) has been accepted. This ticket tracks its implementation.
Along with implementing it, we should also document it in the users' guide (the subject of #15658 (closed)).
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information