blob: b5bd77fcb0d69e0e303b6a0c1284ef441f9051da (
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
|
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{- # OPTIONS_GHC -fno-defer-type-errors #-}
module T13446 where
import Data.Coerce (Coercible)
import Data.Kind (Type, Constraint)
import GHC.TypeLits (Symbol)
data Dict :: Constraint -> Type where
Dict :: a => Dict a
infixr 9 :-
newtype a :- b = Sub (a => Dict b)
instance a => Show (a :- b) where
showsPrec d (Sub Dict) = showParen (d > 10) $ showString "Sub Dict"
class Lifting p f where
lifting :: p a :- p (f a)
data Blah a = Blah
newtype J (a :: JType) = J (Blah (J a))
newtype JComparable a = JComparable (J (T (JTy a)))
instance Lifting JReference JComparable where
lifting = Sub 'a'
class (Coercible a (J (JTy a))) => JReference a where
type JTy a :: JType
type T a
= 'Generic ('Iface "java.lang.Comparable") '[a]
data JType = Class Symbol
| Generic JType [JType]
| Iface Symbol
type JObject = J (Class "java.lang.Object")
instance JReference JObject where
type JTy JObject = 'Class "java.lang.Object"
|