How can I coerce constraints?

Question

Is there any mechanism to coerce constraints in Haskell (beside unsafeCoerce which I hope works)?

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
module CatAdjonctionsSOQuestion where

import Data.Proxy
import Data.Tagged
import Unsafe.Coerce

newtype K a ph = K {unK :: a} -- I would want c a => c ((K a) i) for any c :: Constraints

-- I could do any possible instance by hand
deriving via a instance Semigroup a => Semigroup ((K a) i)

-- I want them all
-- deriving via a instance c ((K a) i) -- Instance head is not headed by a class: c (K a i)

data Exists c where
  Exists :: c a => a -> Exists c

data ExistsKai c i where
  ExistsKai :: c ((K a) i) => Proxy a -> ExistsKai c i

ok :: forall x c i. (forall x. (forall a. c a => a -> x) -> x) -> (forall a. c ((K a) i) => Tagged a x) -> x
ok s k =
  let e = (s Exists :: Exists c)
   in let f = unsafeCoerce e :: ExistsKai c i
       in case f of (ExistsKai (Proxy :: Proxy a)) -> unTagged (k @a)

What exactly are you asking about? `instance c a => c ((K a) b)` strikes me a very bad idea. But this isn't what the title seem to ask anyway. So, ...? — leftaroundabout, May 16 '21 at 13:55
Also, the signature of `ok` looks horrible with those shadowed type variables and all. Can't you simplify the scenario a bit more? (And I personally find `∀` makes such signatures a good deal clearer than `forall`.) — leftaroundabout, May 16 '21 at 13:59
`a` is the "same" as `K a i`. every instance `a` possesses ,`K a I` should possess as well. I can use the `deriving via` for any constraint `c` I imagine, thanks to coercion. So I want to lift every instances I have on `a` to `K a i`. — nicolas, May 16 '21 at 14:41
I agree, it's an ugly signature.. not sure how to make it nicer. I can replace `a` by `proxy a` probably. — nicolas, May 16 '21 at 14:42
just like we can coerce data types to attach a family of instances to a datatype, we could, in principle (I imagine) , quantity over instances and attach them to a family of datatypes. — nicolas, May 16 '21 at 15:04
in my case, I use some internal datatype in a library, but I take constraints from the client. without this, he will have to write the proof that his constraints commute with my datatype. although my internal datatype is just a newtype... — nicolas, May 16 '21 at 15:10
It's an interesting question, and I'm not sure if it's doable. But I will echo what others have already said that, even if it *is* doable, you probably shouldn't. If I saw this code in a Haskell library in the wild, I'd *immediately* discard it and find an alternative library with less magic. — Silvio Mayolo, May 16 '21 at 15:31
@SilvioMayolo I don't disagree, but sometimes you need what you need. what matters is to know why you need dirty stuff and have multiple ways to explain how that's the only way and how it should be part of a better haskell. I am sure there was plenty of unsafeCoerce before coercible — nicolas, May 17 '21 at 15:06
for instance, I wonder if haskell shouldn't provide a generic rank 1 identity wrapper with the said property. — nicolas, May 17 '21 at 15:11

dfeuer · Accepted Answer · 2021-05-17T06:29:40.230

3

With a slight modification to make it kind check, you ask for

newtype K a ph = K {unK :: a}
-- I would want c a => c ((K a) i)
-- for any c :: Type -> Constraint

You absolutely can't get that, now or ever, because it's invalid. Consider

(~) Bool :: Type -> Constraint

Now (~) Bool Bool holds, but you can never achieve (~) Bool (K Bool i).

What about without equality constraints? Well, I can do that too, using Leibniz equality:

class Bar a where
  isBool :: f a -> f Bool

instance Bar Bool where
  isBool = id

But there is no way to write instance Bar (K Bool i) whose isBool doesn't bottom out.

edited May 17 '21 at 06:29

answered May 16 '21 at 16:45

dfeuer

48,079
5
63
167

nice counter example. rephrasing : `deriving via` only **selects** the branch which will be taken. once selected, further equations are introduced for solving. and those have no reason to be verified. *coerce* (thus deriving via) only talks about the data **representation** not at all about the equations attached to the datatype. we do not have a language for these to select out the ones for which it's safe to do so (like no context). each data/newtype is on its own. – nicolas May 16 '21 at 21:40
(unrelated: would appreciate you giving a look at my latest answer/edit with a suspected bug in current `foldr1` implementation were `foldr1 (||) (True : undefined)` apparently diverges, to my surprise. should it really?.... `foldr (||) undefined (True : undefined)` doesn't. I think the two should be equivalent.) – Will Ness May 17 '21 at 06:39
It's too bad we can't do this operation on the subset that haskell forces us to introduce for technical reason. like when you have a type `(f a, b)` and you need (haskell requires you) to see it uniformly as a pair of applied type constructors `(f a, I b)` with `I` some identity newtype. – nicolas May 17 '21 at 15:01
1

@nicolas, I think we might be getting more access to explicit representations of class dictionaries soonish (though I haven't been paying enough attention to the detailed proposals), so maybe eventually. – dfeuer May 18 '21 at 21:32

How can I coerce constraints?

1 Answers1