-- |
-- Module      : Equality
-- License     : BSD-3-Clause
-- Copyright   : (c) 2026 Olivier Chéron
--
-- Generate a constraint @'PrimSize' a ~ 'PrimSize' b@
--
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
module Equality
    ( EqPrimSize, ensureEqPrimSize
    ) where

import Data.Type.Equality

import Base

type EqPrimSize a b = (PrimType a, PrimType b, PrimSize a ~ PrimSize b)

eqPrimSize :: PrimSize a ~ PrimSize b => k a b -> PrimSize a :~: PrimSize b
eqPrimSize :: forall a b (k :: * -> * -> *).
(PrimSize a ~ PrimSize b) =>
k a b -> PrimSize a :~: PrimSize b
eqPrimSize k a b
_ = PrimSize a :~: PrimSize b
PrimSize b :~: PrimSize b
forall {k} (a :: k). a :~: a
Refl

ensureEqPrimSize :: EqPrimSize a b => k a b -> c -> c
ensureEqPrimSize :: forall a b (k :: * -> * -> *) c. EqPrimSize a b => k a b -> c -> c
ensureEqPrimSize k a b
op = case k a b -> PrimSize a :~: PrimSize b
forall a b (k :: * -> * -> *).
(PrimSize a ~ PrimSize b) =>
k a b -> PrimSize a :~: PrimSize b
eqPrimSize k a b
op of PrimSize a :~: PrimSize b
Refl -> c -> c
forall a. a -> a
id