Fcf.hs

-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

module Morley.Util.Fcf
  ( Over2
  , type (<|>)
  , TyEqSing
  , ApplyConstraints
  , Eval
  ) where

import Data.Singletons.Prelude.Eq (DefaultEq)
import Fcf (type Eval, type Exp, type LiftM2)

data Over2 :: (a -> b -> Exp r) -> (x -> Exp a) -> (x -> Exp b) -> x -> Exp r
type instance Eval (Over2 f g h x) = Eval (LiftM2 f (g x) (h x))

data (<|>) :: f a -> f a -> Exp (f a)
type instance Eval ('Nothing <|> m) = m
type instance Eval ('Just x <|> _) = 'Just x

-- | Similar to 'Fcf.TyEq', but compares types via @DefaultEq@ used in singletons
-- comparisons (see "Data.Singletons.Prelude.Eq" module).
data TyEqSing :: a -> b -> Exp Bool
type instance Eval (TyEqSing a b) = DefaultEq a b

data ApplyConstraints :: [a -> Constraint] -> a -> Exp Constraint
type instance Eval (ApplyConstraints '[] _) = (() :: Constraint)
type instance Eval (ApplyConstraints (c ': cs) a) =
  (c a, Eval (ApplyConstraints cs a))