blob: 36edbbc62b1f6ca76adc0ea188fe5303a7f178ce (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language TypeFamilyDependencies #-}
{-# Language GADTs #-}
{-# Language TypeSynonymInstances #-}
{-# Language FlexibleInstances #-}
{-# Language QuantifiedConstraints #-}
module T15943 where
import Data.Type.Equality
import Data.Coerce
import Data.Type.Coercion
import Data.Kind
newtype WrapFalse a b = WrapFalse (Hom False a b)
newtype WrapTrue a b = WrapTrue (Hom True a b)
class
(forall (x :: ob) (y :: ob). Coercible (WrapFalse x y) (WrapTrue y x))
=>
Ríki ob where
type Hom (or::Bool) = (res :: ob -> ob -> Type) | res -> or
instance Ríki Type where
type Hom False = (->)
type Hom True = Op
newtype Op :: Type -> Type -> Type where
Op :: (b -> a) -> Op a b
|
