blob: 7b2b03e713e5f3f7830d0a390d3ce0ec8d385590 (
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
|
{-# Language RankNTypes, TypeApplications, PolyKinds, DataKinds, TypeOperators, StandaloneKindSignatures, TypeFamilies, FlexibleInstances, MultiParamTypeClasses #-}
module T19094 where
import Data.Type.Equality
import Data.Kind
type PolyKinded :: Type -> Type
type PolyKinded res = (forall (k :: Type). k -> res)
infix 4
===
type
(===) :: PolyKinded (PolyKinded Bool)
type family
a === b where
a === a = True
_ === _ = False
type TryUnify :: Bool -> PolyKinded (PolyKinded Constraint)
class (a === b) ~ cond
=> TryUnify cond a b
instance (a === b) ~ False
=> TryUnify False @k a @j b
instance {-# Incoherent #-}
( (a === b) ~ True
, a ~~ b
)
=> TryUnify True @k a @j b
|
