blob: 0169a59bafffb8f62120a469a79ddbbb1aaae9f1 (
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
59
60
61
|
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
-- This nasty example fails with quick-look
-- (which here is switched on by ($))
-- beecause of a very subtle issue where we instantiate an
-- instantiation variable with (F alpha), where F is a type function
--
-- It's a stripped-down version of T5490
register :: forall rs op_ty.
(HDrop rs ~ HSingle (WaitOpResult op_ty))
=> rs -> op_ty
-> Maybe (WaitOpResult (WaitOps rs))
-> Int
register _ _ ev
= ($) -- (px -> qx) -> px -> qx px=a_a2iT qx=b_a2iU
(foo ev) -- Instantiate at ax=a2iW bx=a2iX;
-- (ax,bx) -> Int
-- ql on arg ev bx := WaitOpResult (WaitOps rs) = [rs]
-- px := (ax,bx)
-- qx := Int
(inj 3) -- instantiate lx=l_a2iZ;
-- res_ty (HNth n lx, [lx])
-- res_ty px = (ax,bx) ~ (HNth n lx, [lx])
-- ax := HNth n lx
-- bx := [lx]
-- Result ql: WaitOpResult op_ty ~ ax = HNth n lx
{-
($) @(HNth l0, WR (WO rs))
@Int
(foo ev)
(inj 3)
-}
foo :: forall a b . Maybe b -> (a,b) -> Int
foo = error "urk"
inj :: Int -> (HNth l, [l])
inj = error "urk"
data HSingle a
type family HHead l
type instance HHead (HSingle h) = h
data WaitOps rs
type family WaitOpResult op
type instance WaitOpResult (WaitOps rs) = [rs]
type family HDrop l
type HNth l = HHead (HDrop l)
|
