mldsa-0.1.0.0: src/Equality.hs

-- |
-- 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 _ = Refl

ensureEqPrimSize :: EqPrimSize a b => k a b -> c -> c
ensureEqPrimSize op = case eqPrimSize op of Refl -> id