blob: 0330784a698f54859d4c3511b4e9ed24635aef7e (
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
|
-- This used to produce Core Lint errors
{-# Language ConstraintKinds #-}
{-# Language DataKinds #-}
{-# Language FlexibleInstances #-}
{-# Language GADTs #-}
{-# Language ImpredicativeTypes #-}
{-# Language KindSignatures #-}
{-# Language MultiParamTypeClasses #-}
{-# Language PolyKinds #-}
{-# Language QuantifiedConstraints #-}
{-# Language RankNTypes #-}
{-# Language TypeOperators #-}
{-# Language UndecidableInstances #-}
{-# Options_GHC -dcore-lint #-}
module Dict where
import Data.Kind (Type)
import Data.Maybe (isJust, isNothing)
import Data.Type.Equality ((:~:))
data LoT k where
LoT0 :: LoT Type
(:&&:) :: k -> LoT ks -> LoT (k -> ks)
data Dict cls where
Dict :: cls => Dict cls
class GTE a b x y (f :: LoT kf -> Type) (g :: LoT kg -> Type) where
gTE :: f x -> g y -> Maybe (a :~: b)
class (forall a b. GTE a b (a :&&: LoT0) (b :&&: LoT0) rep rep) => As f rep
instance (forall a b. GTE a b (a :&&: LoT0) (b :&&: LoT0) rep rep) => As f rep
ok :: Dict (As f rep) -> Dict (forall a b. GTE a b (a :&&: LoT0) (b :&&: LoT0) rep rep)
ok Dict = Dict
|
