summaryrefslogtreecommitdiff
path: root/testsuite/tests/typecheck/should_fail/T13446.hs
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"