Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here. I would expect this to work, but it doesn't.

```class Model a b | a -> b where
model :: a -> b

data Temp b where
Temp :: Model a b => b -> Temp a

getTemp :: Model a b => Temp a -> b
getTemp (Temp a) = a
```
```/home/sandy/Vik.hs:11:20: error:
• Couldn't match expected type ‘b’ with actual type ‘b1’
‘b1’ is a rigid type variable bound by
a pattern with constructor:
Temp :: forall a b. Model a b => b -> Temp a,
in an equation for ‘getTemp’
at /home/sandy/Vik.hs:11:10-15
‘b’ is a rigid type variable bound by
the type signature for:
getTemp :: forall a b. Model a b => Temp a -> b
at /home/sandy/Vik.hs:10:1-35
• In the expression: a
In an equation for ‘getTemp’: getTemp (Temp a) = a
• Relevant bindings include
a :: b1 (bound at /home/sandy/Vik.hs:11:15)
getTemp :: Temp a -> b (bound at /home/sandy/Vik.hs:11:1)
|
11 | getTemp (Temp a) = a
|
``` given that `model` is library code i want to interface with, how can i do this? more generally the problem i'm trying to solve is that given some opaque datatype `A` that i can define arbitrarily to my liking, and an instance `Model A B`, i want to write a bunch of code that uses `B` but refers to `A` in the type signature `getTemp (Temp a) = a` is pretty confusing, tripped me up for a minute. It's probably easier to read if you replaced the as with bs :D i want to write code of the form:

```f :: A -> whatever
f = something with (model a)
```

and then invoke it with something like `f (unmodel \$ something of type B)` such that the definition of `A` and `unmodel` are entirely mechanical and require no thought from me whatsoever as the user of this library Because trying out stuff like making it an associated type rather than fundep is out of the question (not even sure if it would fix the problem) this doesnt work :(

```class Model a b => Model2 a where
type TheModel a
instance Model a b => Model2 a where
type TheModel a = b
``` @Sandy Maguire That isn’t a bug in GHC, it’s the way fundeps are designed (for better or for worse). Fundeps don’t provide evidence the way type equalities against type families do, they just affect type inference. What does that mean in practice? It means that if you have

```class C a b | a -> b
instance C Int Bool
```

and you end up with a `C Int a` given, you cannot deduce a `a ~ Bool` given! Instead, all the fundep does is cause a new `a ~ Bool` wanted to be emitted. If `a` is a solver variable, this makes nice things happen: `a` will be solved to `Bool`, and you get nice type inference. But if `a` is rigid, you get nothing: you just end up with an `a ~ Bool` wanted that you cannot solve. You can see this for yourself by writing the following very simple program:

```class C a b | a -> b
instance C Int Bool

foo :: C Int a => a :~: Bool
foo = Refl
```

This program will not compile. You have to think of fundeps as “inference guides,” not sources of evidence. (The formal term for this “inference guiding” is “improvement,” introduced by Mark P. Jones in his work on qualified types.) Unless something fundamental changes in GHC’s treatment of functional dependencies, you will never be able to acquire type equality evidence from a functional dependency alone, since it simply doesn’t exist. The type family equivalent works because you explicitly pass around evidence for a type equality. If you write

```class C1 a where
type B a
instance C1 Int where
type B Int = Bool

class b ~ B a => C2 a b | a -> b
instance (C1 a, b ~ B a) => C2 a b
```

then when you write `foo`, it typechecks because you can get the `a ~ B Int` evidence out of the `C2` dictionary’s superclass dictionaries. (It can be helpful to think of `a ~ b` constraints as implicitly-passed `a :~: b` values, since in GHC, that’s exactly what they are.) apparently i've been away from Hs too long! I didn't even think about passing around `:~:`s maybe it's just because it's early and i'm still in bed, but i don't see how to make this work with explicit Refls either ```newtype Opaque a = Opaque { getOpaque :: a }
deriving (Eq, Ord, Show, Enum, Bounded, Read, Semigroup, Monoid)

instance Arbitrary a => Arbitrary (Opaque a) where
arbitrary = fmap Opaque arbitrary

instance Model (Opaque a) a where
model = getOpaque
```