On Mon, May 7, 2018 at 7:50 AM, Clinton Mead wrote:

class Num t => MyNum t where type IsNum t instance Num t => MyNum t where type IsNum t = Satisfied

This looks wrong to me: given how instance resolution works, I'd expect this to match every type and produce Satisfied, and later rejection based on the context wouldn't affect it. But I could well be thinking about it incorrectly. -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

On Tue, 8 May 2018 at 12:20 AM, Clinton Mead wrote:

Firstly, you refer to https://wiki.haskell.org/GHC/AdvancedOverlap. Unfortunately (unless I've missed something) these involve listing all the instances of parent classes. I'm trying to avoid that. Indeed if I have to explicitly list all the instances I might as well write them the normal way so I'm not sure what the point of any trickery is.

Yes that approach does need declaring instances of `ShowPred` (or in general `XXXPred`), which doubles-up the instances for `Show` (or `XXX`). That approach is making a closed world: for every type `t`, return either `True` or `False` that it has an instance for `Show`. I'm not sure what you mean by "write them the normal way"? Just declaring `t` an instance of `Show` doesn't expose that in any way you can run type-level functions over it.

I also tried the associated types approach you suggested towards the end of your email previously. This works perfectly fine if you can edit the base class, but I can't edit say, "Applicative" or "Num".

Your O.P. talked about classes `A, B`, which I assumed you were writing fresh. What is your use case for wanting `EitherSatisfied (Applicative t) (Num t)` for the same `t`? (Those two classes want a `t` of different kind/arity, for one thing.) I did something like the following, but I ran into a problem:

... class Num t => MyNum t where type IsNum t instance Num t => MyNum t where type IsNum t = Satisfied

No that won't work (as others have pointed out). That `MyNum t` instance makes every type an instance of `MyNum`, so `(IsNum t)` always returns `Satisfied`. And it'll always compile because the instance constraint `Num t` is ignored for associated types. (Note that an Assoc type is just syntactic sugar for a type family, and you can't put constraints on TF equations.)

Any suggestions going forward from here?

I'm puzzled what it is you're trying to do. Your O.P. on the cafe talked about satisfying one or both of two constraints. Neither that nor your StackOverflow original question 'Reducing satisfied constraints to ordinary types' mentioned you want to use this for `Prelude` classes. Which specific classes? There is a ghc extension coming along soon which supports some limited froms of implications over types and instances. I'm not going to suggest it until I know what you're trying to do. I have a nervous feeling that you nurse incorrect expectations. This instance Num t => MyNum t where _does not_ say "if `t` is an instance of `Num`, it's thereby an instance of `MyNum`". It says "every `t` is an instance of `MyNum`; if I use some method from `MyNum` on some particular type `t0`, validate that also `Num t0`". There's a deep reason why Haskell works like that. See my added note to the SO answer. AntC

On Tue, 8 May 2018 at 2:00 PM, Clinton Mead wrote:

On Tue, May 8, 2018 at 11:17 AM, Anthony Clayden < anthony_clayden@clear.net.nz> wrote:

...

On Tue, 8 May 2018 at 12:20 AM, Clinton Mead wrote:

...

Firstly, you refer to https://wiki.haskell.org/GHC/AdvancedOverlap. Unfortunately (unless I've missed something) these involve listing all the instances of parent classes. I'm trying to avoid that. Indeed if I have to explicitly list all the instances I might as well write them the normal way so I'm not sure what the point of any trickery is.

Yes that approach does need declaring instances of `ShowPred` (or in general `XXXPred`), which doubles-up the instances for `Show` (or `XXX`). That approach is making a closed world: for every type `t`, return either `True` or `False` that it has an instance for `Show`.

I'm not sure what you mean by "write them the normal way"? Just declaring `t` an instance of `Show` doesn't expose that in any way you can run type-level functions over it.

By normal way as in if I need to list every instance as "ShowPred", I might as well just scrap "ShowPred" and just write them directly as instances of "Print". i.e.

No you haven't got it: there's a default/fallback instance for `Print` that applies if `ShowPred` comes out `False`. Also if you have `True/False` you can do Boolean logic over the result: type instance ShowPred [a] = ShowPred a -- implication type instance ShowPred (a, b) = And (ShowPred a) (ShowPred b) -- conjunction including either/or logic, which is where your O.P. started. (Although we seem to have come a long way from that.) So turning to your latest example ...

...

I'm puzzled what it is you're trying to do.

I'm trying to select instances based on whether constraints are fulfilled.

... consider:

class Join' m (IsSatisfied m) (IsSatisfied m) => Join m where join :: m (m a) -> m a

instance Join' m (IsSatisfied m) (IsSatisfied m) => Join m where join = join'

?? I think that context needs something like instance Join' m (IsMonad m) (IsComonad m) => Join m where ...

instance Monad m => Join' m Satisfied t2 where join' x = x >>= id

instance Comonad m => Join' m t1 Satisfied where join' = extract

instance Comonad m => Join' m Satisfied Satisfied where join' = extract

So if some `m0` is both a `Comonad` and a `Monad`, you want to prefer the `Comonad` method. If `m0` is a `Monad` but not a `Comonad`, use the `Monad` method. You've just invoked a closed world: you're relying on the compiler determining some `m0` is _not_ a `Comonad`. Technically: your instances for `Join'` overlap. So the compiler's inference selection must determine which is the more specific, given some particular `m0` with its `t1, t2` result from `IsSatisfied`. It can select head `Join' m Satisfied t2` only if it can prove `t2` is apart from `Satisfied`. ...

"IsSatisfied" only needs to assert when the constraint is satisfied, it doesn't need to assert when it isn't, ...

Yes it does for what you're asking to do. so I don't think it violates the open world assumption. Also GHC has this

information to give an answer to IsSatisfied, it simply has to try to solve the constraint and if it succeeds reduce it to Satisfied, and if it doesn't it just does nothing.

To the contrary: what you want it to do is select a different instance. AntC