Instance.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
module Language.LOL.Typing.Lib.Control.Monad.Classes.Instance where
import Data.Bool (Bool(..))
import GHC.Prim (Constraint)

-- | A data type to existentially wrap a value of type @ty@,
-- when it is an instance of the type class @cl@.
data Instance (cl:: * -> Constraint)
 = forall ty. cl ty => Instance ty

-- | An open type family to know (at the type level) whether a type @ty@
-- has an instance of the type class @cl@.
--
-- NOTE: currently, users have to manually define type family instances of 'Class'
-- to indicate to the compiler which type support which type class.
-- It is definitively redundant to have to define
-- both a type class instance and a type family instance,
-- but I cannot find a way to automatically synchronize
-- the compiler's knowledge between these two levels.
type family Class (cl:: * -> Constraint) (ty:: *) :: Bool