blob: 746c6448ef8b8d715bf9f923a799495f4bc1684e (
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
62
63
64
65
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module T12444 where
data Nat = Zero | Succ Nat
data SNat (n :: Nat) where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
type family (:+:) (a :: Nat) (b :: Nat) :: Nat where
m :+: Zero = m
m :+: (Succ n) = Succ (m :+: n)
foo :: SNat (Succ c) -> SNat b -> SNat (Succ (c :+: b))
foo _ x = x
{-
sadd :: ((Succ n1 :+: n) ~ Succ (n1 :+: n), (Succ n1) ~ m)
=> SNat m -> SNat n -> SNat (m :+: n)
sadd SZero n = n
-}
{- [G] a ~ Succ c
Succ c + b ~ Succ (c+b)
a ~ Zero
-->
Zero ~ Succ c TyEq
fsk1 ~ Succ fsk2 TyEq
fsk1 ~ (Succ c) + b FunEq
fsk2 ~ c+b FunEq
----
[W] b ~ a+b ---> b ~ Succ (c+b)
Derived
a ~ Succ c
fsk1 ~ Succ fsk2
b ~ Succ fsk2
work (Succ c) + b ~ fsk1
c+b ~ fsk2
-}
{-
[G] a ~ [b]
--> Derived shadow [D] a ~ [b]
When adding this to the model
don't kick out a derived shadow again!
[G] (a ~ b) --> sc a ~~ b, a ~# b
Silly to then kick out (a~b) and (a~~b)
and rewrite them to (a~a) and (a~~a)
Insoluble constraint does not halt solving;
indeed derived version stays. somehow
-}
|
