Functionally dependant wrapped in a newtype

Question

I wonder why the below code does not compile and if there is an implementation mkYVal that GHC would accept.

class C x y | x -> y
newtype YVal x = YVal { getYVal :: forall y . C x y => y }
mkYVal :: C x y => y -> YVal x
mkYVal y = YVal y

I also tried

mkYVal :: (y  ~ y1, C x y1) => y -> YVal x
mkYVal y = YVal y

But it still sais

[...]: error:
  • Couldn't match type ‘y2’ with ‘y1’
      ‘y2’ is a rigid type variable bound by
        a type expected by the context:
          forall y2. C x y2 => y2
        at [...]
      ‘y1’ is a rigid type variable bound by
        the type signature for:
          mkYVal :: forall y y1 x. (y ~ y1, C x y1) => y -> YVal x
        at [...]
      Expected type: y2
        Actual type: y
    • In the first argument of ‘YVal’, namely ‘y’
      In the expression: YVal y
      In an equation for ‘mkYVal’: mkYVal y = YVal y
...

Critchfield

This is one of my pet peeves about fundeps. Having a context C x y1, C x y2 does not imply y1 ~ y2 as one might expect. Indeed, one might expect that foo :: (C x y1, C x y2) => y1 :~: y2 ; foo = Refl compiles, but it does not. – Ultimogeniture

Consider type families instead of fundeps, it is rather straightforward with this extension. – Whithersoever

C was actually MonadReader in my particular case. Anyway I have a workaround, I was just sad that this solution didn't work... – Critchfield