blob: 0d3a94f9c90fec2e12d9e6b40ee46e9ee51be382 (
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
|
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies, GADTs, PolyKinds, DataKinds, ExplicitForAll #-}
-- See also: saks007_fail.hs
module SAKS_007 where
import Data.Kind (Type, Constraint)
type family F a where { F Type = True; F _ = False }
type family G a where { G Type = False; G _ = True }
type X :: forall k1 k2. (F k1 ~ G k2) => k1 -> k2 -> Type
data X a b where
MkX :: X Integer Maybe -- OK: F Type ~ G (Type -> Type)
-- True ~ True
{-
Let co :: F Type ~ G (Type->Type)
Wrapper data con type:
$WMkX :: X @Type @(Type->Type) @(Eq# co) Integer Maybe
Worker data con's type:
MkX :: forall k1 k2 (c :: F k1 ~ G k2) (a :: k1) (b :: k2)
-> forall . -- No existentials
( k1 ~# Type, k2 ~# Type->Type -- EqSpec
, a ~# Integer, b ~# Maybe )
=> X k1 k2 c a b
f :: forall k. (k ~ Type) => forall (a::k). a->a
f :: forall (cv :: a ~# b) => ....ty|>co....
X @kk1 @kk2 @(d :: F kk1 ~ G kk2) Integer Maybe
-}
|
