blob: eb3c700f9f357aa63c2984c52f4ab202189b87c0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
{-# Language RankNTypes, ConstraintKinds, TypeInType, GADTs #-}
module T14939 where
import Data.Kind
type Cat ob = ob -> ob -> Type
type Alg cls ob = ob
newtype Frí (cls::Type -> Constraint) :: (Type -> Alg cls Type) where
Frí :: { with :: forall x. cls x => (a -> x) -> x }
-> Frí cls a
data AlgCat (cls::Type -> Constraint) :: Cat (Alg cls Type) where
AlgCat :: (cls a, cls b) => (a -> b) -> AlgCat cls a b
leftAdj :: AlgCat cls (Frí cls a) b -> (a -> b)
leftAdj (AlgCat f) a = undefined
|
