contraintes INFER à la fois si et bien de type égalité

Question

Je suis en train de remplir le trou dans l'extrait suivant

import Data.Proxy 
import GHC.TypeLits 
import Data.Type.Equality 
import Data.Type.Bool 
import Unsafe.Coerce 

ifThenElse :: forall (a :: Nat) (b :: Nat) x l r. 
    (KnownNat a, KnownNat b, x ~ If (a==b) l r) => 
    Proxy a -> Proxy b -> Either (x :~: l) (x :~: r) 
ifThenElse pa pb = case sameNat pa pb of 
    Just Refl -> Left Refl 
    Nothing -> Right $ unsafeCoerce Refl -- This was the hole 

Est-il possible?

Modifier: Vérifié la source de sameNat et il s'avère qu'ils utilisent unsafeCoerce. J'ai modifié le code ci-dessus en conséquence.

Answer 1

Une solution possible consiste à utiliser la bibliothèque singletons pour obtenir des fonctions de niveau terme représentant les fonctions de niveau (ou vice versa).

L'essentiel de c'est:

import Data.Singletons.Prelude 

(...)

case (sing :: Sing a) %:== (sing :: Sing b) of 
    STrue -> Left Refl 
    SFalse -> Right Refl 

J'ai mis un self-contained file toutes les importations et les extensions de langage aussi.