blob: 077c80c490fc189210400738eec5fbacf0d679b2 (
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
{-# OPTIONS_GHC -fdefer-type-errors #-} -- Very important to this bug!
{-# Language PartialTypeSignatures #-}
{-# Language TypeFamilyDependencies, KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language DataKinds #-}
{-# Language TypeFamilies #-}
{-# Language RankNTypes #-}
{-# Language NoImplicitPrelude #-}
{-# Language FlexibleContexts #-}
{-# Language MultiParamTypeClasses #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}
{-# Language FlexibleInstances #-}
{-# Language TypeOperators #-}
{-# Language ScopedTypeVariables #-}
{-# Language DefaultSignatures #-}
{-# Language FunctionalDependencies #-}
{-# Language UndecidableSuperClasses #-}
{-# Language UndecidableInstances #-}
{-# Language AllowAmbiguousTypes #-}
{-# Language InstanceSigs, TypeApplications #-}
module T14584 where
import Data.Monoid
import Data.Kind
import Data.Type.Equality
data family Sing (a::k)
class SingKind k where
type Demote k = (res :: Type) | res -> k
fromSing :: Sing (a::k) -> Demote k
class SingI (a::k) where
sing :: Sing a
data ACT :: Type -> Type -> Type
data MHOM :: Type -> Type -> Type
type m %%- a = ACT m a -> Type
type m %%-> m' = MHOM m m' -> Type
class Monoid m => Action (act :: m %%- a) where
act :: m -> (a -> a)
class (Monoid m, Monoid m') => MonHom (mhom :: m %%-> m') where
monHom :: m -> m'
data MonHom_Distributive m :: (m %%- a) -> (a %%-> a)
type Good k = (Demote k ~ k, SingKind k)
instance (Action act, Monoid a, Good m) => MonHom (MonHom_Distributive m act :: a %%-> a) where
monHom :: a -> a
monHom = act @_ @_ @act (fromSing @m (sing @m @a :: Sing _))
|
