{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Hask.Eq where

import Data.Type.Equality ((:~:)(..))
import Hask.Core

type family (==) :: i -> i -> j
type instance (==) = (~)   -- @k -> k -> Constraint@
type instance (==) = (:~:) -- @k -> k -> *@

class hom ~ Hom => Subst (hom :: j -> j -> k) where
  subst :: Hom (a == b) (hom (f a) (f b))

instance Subst (:-) where
  subst Refl = id

instance Subst (->) where
  subst Refl = id

instance Subst (|-) where
  subst = go where
    go :: forall f a b. (a == b) :- (f a |- f b)
    go = Sub $ Dict \\ (jot :: () :- f a |- f a)