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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
|
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE QuantifiedConstraints #-}
module T14961 where
import Data.Kind
import Control.Arrow (left, right, (&&&), (|||))
import Control.Category
import Prelude hiding (id, (.))
import Data.Coerce
class (forall x. f x => g x) => f ~=> g
instance (forall x. f x => g x) => f ~=> g
type family (#) (p :: Type -> Type -> Type) (ab :: (Type, Type))
= (r :: Type) | r -> p ab where
p # '(a, b) = p a b
newtype Glass
:: ((Type -> Type -> Type) -> Constraint)
-> (Type, Type) -> (Type, Type) -> Type where
Glass :: (forall p. z p => p # ab -> p # st) -> Glass z st ab
data A_Prism
type family ConstraintOf (tag :: Type)
= (r :: (Type -> Type -> Type) -> Constraint) where
ConstraintOf A_Prism = Choice
_Left0
:: Glass Choice
'(Either a x, Either b x)
'(a, b)
_Left0 = Glass left'
_Left1
:: c ~=> Choice
=> Glass c '(Either a x, Either b x) '(a, b)
_Left1 = Glass left'
-- fails with
-- • Could not deduce (Choice p)
-- _Left2
-- :: (forall p. c p => ConstraintOf A_Prism p)
-- => Glass c '(Either a x, Either b x) '(a, b)
-- _Left2 = Glass left'
_Left3
:: d ~ ConstraintOf A_Prism
=> (forall p . c p => d p)
=> Glass c
'(Either a x, Either b x)
'(a, b)
_Left3 = Glass left'
-- fails to typecheck unless at least a partial type signature is provided
-- l :: c ~=> Choice => Glass c _ _
-- l = _Left1 . _Left1
newtype Optic o st ab where
Optic
:: (forall c d. (d ~ ConstraintOf o, c ~=> d) => Glass c st ab)
-> Optic o st ab
_Left
:: Optic A_Prism
'(Either a x, Either b x)
'(a, b)
_Left = Optic _Left1
instance Category (Glass z) where
id :: Glass z a a
id = Glass id
(.) :: Glass z uv ab -> Glass z st uv -> Glass z st ab
Glass abuv . Glass uvst = Glass (uvst . abuv)
class Profunctor (p :: Type -> Type -> Type) where
dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
lmap :: (a -> b) -> p b c -> p a c
rmap :: (b -> c) -> p a b -> p a c
class Profunctor p => Choice (p :: Type -> Type -> Type) where
left' :: p a b -> p (Either a c) (Either b c)
right' :: p a b -> p (Either c a) (Either c b)
|
