haskellderivingderivingvia# How can I coerce constraints?

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)
```

Solution

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.

- Comparing lists in Haskell
- Is there a non-identity monad morphism M ~> M that is monadically natural in M?
- Problem with loading module ‘Distribution.Simple’
- Improving efficiency in Stirling numbers calculation
- Does sequencing an infinite list of IO actions by definition result in a never-ending action? Or is there a way to bail out?
- How to call pgQuery from postgresql-query?
- How to avoid whitespace after a tag (link) in Hamlet templates?
- Understanding type-directed resolution in Haskell with existential types
- Why is seq bad?
- Understanding bind function in Haskell
- How to create route that will trigger on any path in Servant?
- How do I use a global state in WAI middleware?
- nixos 23.11 cabal install mysql-simple problem - "Missing (or bad) C libraries"
- Is there a way to kill all forked threads in a GHCi session without restarting it?
- Why can an invalid list expression such as 2:1 be assigned to a variable, but not printed?
- Iterate over a type level list and call a function based on each type in the list
- How does this solution of Project Euler Problem 27 in the Haskell Wiki work?
- Why `Monad` is required to use `pure`?
- Can't do partial function definitions in GHCi
- recommended way to convert Double -> Float in Haskell
- Haskell profiling understanding cost centre summary for anonymous lambda
- Why is Haskell fully declarative?
- GHC Generating Redundant Core Operations
- Question about Event firing in reflex-frp
- Using Haskell's "Maybe", type declarations
- How can I elegantly invert a Map's keys and values?
- Why there is no output for wrapped IO in Haskell?
- What are the definitions of Weather and Memory in xmobar repo?
- Serializing a Data.Text value to a ByteString without unnecessary \NUL bytes
- Using Haskell with VS Code