[Haskell-cafe] Constraining constraints

[Ivan Lazar Miljenovic]

On 7 May 2017 at 14:19, Clinton Mead <clintonmead at gmail.com> wrote:
> I posted the following on stackoverflow, but it hasn't got too much
> attention so I thought I'd ask here:
>
> I can write the following:
>
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE UndecidableInstances #-}
> {-# LANGUAGE ConstraintKinds #-}
>
> f :: Integral a => (forall b. Num b => b) -> a
> f = id
>
> And all is good. Presumably GHC can derive Integral from Num so all is well.
>
> I can be a bit tricker, yet I'm still fine:
>
> class Integral x => MyIntegral x
> instance Integral x => MyIntegral x
>
> class Num x => MyNum x
> instance Num x => MyNum x
>
> f' :: MyIntegral a => (forall b. MyNum b => b) -> a
> f' = id

This one I'm not that sure about.

Ignore the actual instances you've provided (since IIRC GHC doesn't
actually look at those for constraints, just the class definition).
Whilst any MyIntegral is an Integral and hence a Num, and likewise any
MyNum is a Num, it doesn't mean that something that creates a MyNum
will be able to create a MyIntegral (e.g. MyNum ~ Floating and you
pass in pi as the value in the forall).

>
> So lets say I want to generalise this, like so:
>
> g :: c2 a => (forall b. c1 b => b) -> a
> g = id
>
> Now obviously this will spit the dummy, because GHC can not derive c2 from
> c1, as c2 is not constrained.
>
> What do I need to add to the type signature of g to say that "you can derive
> c2 from c1"?
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.



-- 
Ivan Lazar Miljenovic
Ivan.Miljenovic at gmail.com
http://IvanMiljenovic.wordpress.com