Faire une contrainte de Maybe a où Eq a

Question

Comment puis-je contraindre à Maybe a où Eq a ? Il faut que ce soit du type * -> Contrainte

Ce que j'ai essayé :

class (a ~ Maybe b, Eq b) => K a where
instance (a ~ Maybe b, Eq b) => K a where

Erreur :

Not in scope: type variable ‘b’

Exemple d'utilisation :

data Test c = forall a. (c a) => Test a
r :: Test K -> Maybe Bool
r (Test o) = (==) <$> o <*> o -- I need GHC to infer that o is Maybe Eq

Des cas qui fonctionnent :

pp :: Test ((~) String) -> String
pp (Test o) = o ++ "X" -- GHC infers that o is a string

hh :: Test Eq -> Bool
hh (Test o) = o == o -- GHC infers that o is Eq

Réponse générique ici : Existe-t-il un moyen général d'appliquer des contraintes à une application de type ?

Answer 1

Ce qui suit se compile sur ma machine. Je n'ai aucune idée de sa pertinence.

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ConstraintKinds #-}
class (Eq (UnMaybe a), a ~ Maybe (UnMaybe a)) => EqMaybe a where
    type UnMaybe a

instance Eq a => EqMaybe (Maybe a) where
    type UnMaybe (Maybe a) = a

data Test c = forall a. c a => Test a
r :: Test EqMaybe -> Maybe Bool
r (Test o) = (==) <$> o <*> o
f :: Test Eq -> Test EqMaybe
f (Test o) = Test (Just o)

Answer 2

Il s'agit d'un problème connu . GHC s'étouffe car vous avez introduit un nouveau type de variable b qui n'est mentionné nulle part ailleurs dans la tête de l'instance. Une solution de contournement consiste à utiliser des familles de types et des types de contraintes.

{-# LANGUAGE ConstraintKinds, TypeFamilies, UndecideableInstances, 
             UndecideableSuperclasses, FlexibleInstances
  #-}

import GHC.Exts (Constraint)
import GHC.Prim (Any)

type family MaybeEq x :: Constraint where
  MaybeEq (Maybe a) = Eq a
  MaybeEq _         = Any    -- A good "unsatisfiable" constraint

class MaybeEq a => K a where
instance MaybeEq a => K a where