instantiating visible parameters in when deriving instances

[Richard Eisenberg]

On Mar 29, 2016, at 3:58 PM, Ryan Scott <ryan.gl.scott at gmail.com> wrote:

> I hope this is a bug and not a fundamental limitation.

As I posted in the ticket, this is a somewhat fundamental limitation. I qualify by "somewhat" because it's a consequence of a design choice, but reversing the design choice would be rather difficult and lead to several more tough design choices. It's my hope and belief that this restriction will one day be lifted. That day will not be soon. The wiki (https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unliftedequality) has some thoughts on the issue, but those notes may be out of date and/or wrong. YMMV.

As for Simon's question about the difference between visible and invisible: when the user says `deriving (Cat k)`, the user has written k and presumably means k to be universally quantified. When the user days `deriving Category`, then no `k` has been written and unification seems appropriate. Of course, if we consider that in the `deriving (Cat k)` case, we're just inferring a `k ~ *` constraint, perhaps this is OK. But it's certainly a bit odd.

Richard