# Why/how does this class/method work? (\`~\` constraint)

**URL:** <https://discourse.haskell.org/t/why-how-does-this-class-method-work-constraint/9117>\
**Category:** Learn\
**Created:** [March 20, 2024, 11:54pm UTC](https://discourse.haskell.org/t/why-how-does-this-class-method-work-constraint/9117 "2024-03-20T23:54:12Z")\
**Posts on this page:** 8\
**Page:** 1

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [March 20, 2024, 11:54pm UTC](https://discourse.haskell.org/t/why-how-does-this-class-method-work-constraint/9117/1 "2024-03-20T23:54:12Z")

</div>

Continuing the discussion from [(… cont) Data.Set no Functor/Monad instance](http://discourse.haskell.org/t/cont-data-set-no-functor-monad-instance/9098):

I threw down this code without much thought just to get something working. (I was quite surprised it worked, and even more surprised the `OVERLAPPABLE` instance works smoothly.)

```haskell
    class Functorb (fb :: Type) where
        fmapb :: fb ~ (f b) => (a -> b) -> f a -> f b 
    
    instance Ord b => Functorb (Set b) where -- with Ord b accepted
        fmapb = mapSet

    instance {-# OVERLAPPABLE #-} Functor f => Functorb (f b) where -- with Functor f accepted
        fmapb = fmap

```

- in the class decl, the parameter `fb` doesn’t appear in the matrix of the method, but only in a constraint. Then
- given some usage site of method `fmapb`, how does instance resolution ‘know’ which instance to select?
- The class works just as well it seems (and that’s less of a surprise) with

```haskell
        fmapb :: fb ~ (f b) => (a -> b) -> f a -> fb -- result type is class param

```

- Is `~` so magic that the method sig I first wrote is interpreted as the second?

---

<div class="post-metadata">

**Author:** ![adamgundry](https://avatars.discourse-cdn.com/v4/letter/a/34f0e0/32.png) [@adamgundry](https://discourse.haskell.org/u/adamgundry)\
**Post date:** [March 22, 2024, 7:59am UTC](https://discourse.haskell.org/t/why-how-does-this-class-method-work-constraint/9117/2 "2024-03-22T07:59:26Z")

</div>

> [@AntC2](#):
>
> given some usage site of method `fmapb`, how does instance resolution ‘know’ which instance to select?

At a use site, we have `fmapb :: (Functorb fb, fb ~ f b) => (a -> b) -> f a -> f b`, which is roughly equivalent to `(Functorb (f b)) => (a -> b) -> f a -> f b`. So if the context determines `f` and `b`, then the appropriate instance can be selected.

More precisely, the magic that occurs with the first version is that GHC will introduce unification variables for `f`, `a`, `b` and `fb`, plus “wanted” constraints `Functor fb` and `fb ~ f b`. Solving the constraint `fb ~ f b` is trivial just by defining `fb := f b`, so `fb` gets substituted out.

> [@AntC2](#):
>
> Is `~` so magic that the method sig I first wrote is interpreted as the second?

The signature itself is not directly re-interpreted due to the presence of the equality constraint. But at use sites, the equality constraint will always be solved by the constraint solver, so they end up being equivalent in practice.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [March 24, 2024, 9:02am UTC](https://discourse.haskell.org/t/why-how-does-this-class-method-work-constraint/9117/3 "2024-03-24T09:02:50Z")

</div>

> [@adamgundry](#):
>
> the equality constraint will always be solved by the constraint solver, so they [the two versions of the sig] end up being equivalent in practice.

Thanks Adam. So equality constraints are solved more eagerly than common-or-garden constraints? (I’m thinking of the `Functor f` or `Ord b` that arises from the rhs of the instances’ equations.)

In particular, instead of `~`, I’ve tried using FunDep-driven `TypeCast` constraints. All I get is `rigid type variable` complaints, because (presumably) GHC won’t do the `fb := f b` step for ordinary constraints.

---

<div class="post-metadata">

**Author:** ![adamgundry](https://avatars.discourse-cdn.com/v4/letter/a/34f0e0/32.png) [@adamgundry](https://discourse.haskell.org/u/adamgundry)\
**Post date:** [March 25, 2024, 8:21am UTC](https://discourse.haskell.org/t/why-how-does-this-class-method-work-constraint/9117/4 "2024-03-25T08:21:29Z")

</div>

GHC tries to find “most general solutions” to constraints, i.e. solutions that cannot be invalidated by information that may come along later. So if it sees wanted constraints `Functorb fb` and `fb ~ f b` then the former has no most general solution (because it is not clear which instance to pick), but the latter can always be solved by taking `fb := f b` (because any solution to the constraints must necessarily include that unification).

Thus the order in which constraints are solved is dynamic, because solving one constraint may make another previously-stuck constraint amenable to solution. In general equality constraints tend to get solved first, because their solutions are usually simple unifications, but this isn’t always true (e.g. if you have an equality constraint between two type families, unification may get stuck).

(Actually for compile-time performance reasons GHC tries to solve simple equality constraints by unification as early as possible, rather than strictly separating the steps to “generate a set of constraints” followed by “solve the constraints”. But the conceptual model is that it the type-checker generates a big set of constraints by walking the syntax tree, then the constraint-solver tries to solve them.)

What does your `TypeCast` class look like?

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [March 25, 2024, 11:08am UTC](https://discourse.haskell.org/t/why-how-does-this-class-method-work-constraint/9117/5 "2024-03-25T11:08:05Z")

</div>

> [@adamgundry](#):
>
> What does your `TypeCast` class look like?

Oh, standard-issue per [HList 2004 Appendix D](https://okmij.org/ftp/Haskell/HList-ext.pdf):

```haskell
module TypeCast where

    class TypeCast a a' | a -> a', a' -> a where
      typeCast :: a -> a'
    instance (TypeCast' () a a') => TypeCast a a' where
      typeCast = typeCast' ()
    class TypeCast' u a a' | u a -> a', u a' -> a where
      typeCast' :: u -> a -> a'
    instance (TypeCast'' u a a') => TypeCast' u a a' where
      typeCast' = typeCast''
    class TypeCast'' u a a' | u a -> a', u a' -> a where
      typeCast'' :: u -> a -> a'
    instance TypeCast'' () a a where
      typeCast'' _ x = x
    

```

> [@adamgundry](#):
>
> [a `~` constraint] can always be solved by taking `fb := f b`

Yeah. `TypeCast` goes through those extra two class indirections deliberately to avoid unifying too early: the equation `fmapb = mapSet` would give too specific `:: (a -> b) -> Set a -> Set b` whereas substituting the instance header’s `(Set b)` for the class’s `fb` wants `(Functorb (Set b), TypeCast (f b1) (Set b)) => (a -> b1) -> f a -> f b1`

```haskell
    * Couldn't match type `f' with `Set'
      `f' is a rigid type variable bound by
        the type signature for:
          fmapb :: forall (f :: * -> *) b1 a.
                   TypeCast (f b1) (Set b) =>
                   (a -> b1) -> f a -> f b1

```

(Usually I can hack my way through rigid tv complaints, but I think the `fb` being ungrounded in the method sig’s matrix makes it all too ethereal. Switching round the order of args to `TypeCast` doesn’t help; sprinking a few calls to the `typeCast` method doesn’t either.)

Thank you for your explanations. I’m an antediluvian hacker, I know. I have a reason for wanting to translate this to Hugs, which I’ll put here if I can get it to work.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [March 26, 2024, 4:21am UTC](https://discourse.haskell.org/t/why-how-does-this-class-method-work-constraint/9117/6 "2024-03-26T04:21:17Z")

</div>

> [@adamgundry](#):
>
> [wanted `fb ~ f b`] can always be solved by taking `fb := f b` (because any solution to the constraints must necessarily include that unification).

mmm? not so fast. We’re at a specific usage site having allocated skolems so we want some `fb0 ~ f0 b0`. It’s not legit to take `fb0 := f0 b0` if `fb0` already has some assignment/unless that is of the form `f1 b1` both skolems not ground types. Neither can we switcheroo `f0 b0 := fb0` unless `fb0` is of the form `f1 b1` and contrariwise `f0 b0` are both skolems.

Or … “because any solution … must necessarily include …” if we make that assignment without checking, then later arrive at a contradiction (ground type mis-match), we’re only exposing a contradiction that was lurking all along. Then the only bit that might have suffered is that the error reporting is maybe remote from the source of confusion(?)

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [March 26, 2024, 5:03am UTC](https://discourse.haskell.org/t/why-how-does-this-class-method-work-constraint/9117/7 "2024-03-26T05:03:00Z")

</div>

> [@AntC2](#):
>
> I have a reason for wanting to translate this to Hugs, which I’ll put here if I can get it to work.

Ok I’ve got working what I wanted to demonstrate. I’ve reverted to a Keep It Simple, Stupid version of the constructor classes, using MultiParams but not FunDeps:

```haskell
    class Functorb f b where -- f :: Type -> Type
        fmapb :: (a -> b) -> f a -> f b 
    
    instance {-# OVERLAPPABLE #-} Functor f => Functorb f b where        
        fmapb = fmap
    
    instance Ord b => Functorb Set b where -- with Ord b accepted
        fmapb = mapSet

```

The objective was instances for a datatype with constraints

```haskell
    newtype Ord b => OrdSet b = MkOrdSet {unOrdSet :: (Set b)} -- cheating; for demo only
                    deriving (Show)
    
    mapOrdSet :: (Ord b) => (a -> b) -> OrdSet a -> OrdSet b -- per H98 needs Ord a from LHS appearance of MkOrdSet
    mapOrdSet f (MkOrdSet s) = MkOrdSet $ mapSet f s       

    instance Ord b => Functorb OrdSet b where -- with Ord b only
        fmapb = mapOrdSet                       
    

```

How did I avoid the `Ord a` constraint on the incoming `OrdSet a`? I ‘reverted’ Hugs to [pre-99 GHC](http://web.archive.org/web/20151001142647/http://code.haskell.org/~dons/haskell-1990-2000/msg04061.html).

> _application_ of MkT as _introducing_ a constraint – hence the type of MkT –  
> but _pattern-matching_ on MkT as _eliminating_ a constraint.  
> But since the dictionary isn’t stored in the constructor [there’s nothing to eliminate, no-op]

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [March 26, 2024, 6:39am UTC](https://discourse.haskell.org/t/why-how-does-this-class-method-work-constraint/9117/8 "2024-03-26T06:39:46Z")

</div>

> [@AntC2](#):
>
> mmm? not so fast. We’re at a specific usage site having allocated skolems

They’d be skolems inside a definition of `fmapb`, but at the use site they’re unknowns, not skolems. (Maybe `f` and `b` have been unified with skolems, but `fb` at least, not appearing in any unifiable part of the signature, must be an unknown.)