blob: 4869e9559df4eae7367730fa877fd82dc4fe99d5 (
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
47
48
49
50
51
52
53
54
55
56
57
58
|
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module T17139 where
import T17139a
type family TypeFam f fun where
TypeFam f (a -> b) = f a -> TypeFam f b
lift :: (a -> b) -> TypeFam f (a -> b)
lift f = \x -> _ (f <*> x)
{-
x :: alpha
body of lambda :: beta
[W] TypeFam f (a->b) ~ (alpha -> beta)
-->
[W] (f a -> TypeFam f b) ~ (alpha -> beta)
-->
alpha := f a
beta := TypeFam f b
(<*>) :: Applicative g => g (p -> q) -> g p -> g q
f <*> x
arg1
(a->b) ~ g0 (p0->q0)
g0 := ((->) a)
(p0 -> q0) ~ b <---------
arg2
alpha ~ g0 p0
g0 ~ f <----------
p0 := a
res
g0 q0
Finish with
[W] f ~ (->) a
[W] b ~ (a -> q0)
--> rewrite b
[W] (a -> q0) ~ a -> (
_ :: g0 q0 -> beta
:: (a -> q0) -> TypeFam f b
:: (a -> q0) -> TypeFam ((->) a) (a -> q0)
:: (a -> q0) -> (a->a) -> TypeFam (-> a) q0
BUT we would get different error messages if we did
g0 := f
and then encountered [W] g0 ~ ((->) a)
-}
|
