blob: a6840ff61642e4847358173c11c9e33a68612f26 (
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
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where
import Data.Kind
-- type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
type SingFunction2 f = forall t1. Sing t1 -> forall t2. Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> SLambda (f x))
type family Sing :: k -> Type
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
data Sym4 a
data Sym3 a
type instance Apply Sym3 _ = Sym4
newtype SLambda (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
type instance Sing = SLambda
und :: a
und = undefined
data E
data ShowCharSym0 :: E ~> E ~> E
sShow_tuple :: SLambda Sym4
sShow_tuple
= applySing (singFun2 @Sym3 (\x -> und x))
(und (singFun2 @Sym3
(\y -> und (applySing (singFun2 @Sym3 (\x -> und x))
(applySing (singFun2 @ShowCharSym0 (\x -> und x)) und)) y)))
|
