Skip to content

Commit 68d1340

Browse files
spcfoxspcfox
authored
[ fix ] Process PiInfo in convert and unify (#3541)
1 parent e443189 commit 68d1340

File tree

14 files changed

+586
-68
lines changed

14 files changed

+586
-68
lines changed

‎CHANGELOG_NEXT.md‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -87,6 +87,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
8787

8888
* Elaborator scripts were made to be able to get pretty-printed resugared expressions.
8989

90+
* Fixed unification and conversion of binders with different `PiInfo`.
91+
9092
### Compiler changes
9193

9294
* The compiler now differentiates between "package search path" and "package

‎src/Core/Normalise/Convert.idr‎

Lines changed: 19 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -319,23 +319,30 @@ mutual
319319
else pure False
320320
chkConvHead q i defs env _ _ = pure False
321321

322+
convPiInfo : {auto c : Ref Ctxt Defs} ->
323+
{vars : _} ->
324+
Ref QVar Int -> Bool -> Defs -> Env Term vars ->
325+
PiInfo (Closure vars) -> PiInfo (Closure vars) -> Core Bool
326+
convPiInfo q i defs env Implicit Implicit = pure True
327+
convPiInfo q i defs env Explicit Explicit = pure True
328+
convPiInfo q i defs env AutoImplicit AutoImplicit = pure True
329+
convPiInfo q i defs env (DefImplicit x) (DefImplicit y) = convGen q i defs env x y
330+
convPiInfo q i defs env _ _ = pure False
331+
322332
convBinders : {auto c : Ref Ctxt Defs} ->
323333
{vars : _} ->
324334
Ref QVar Int -> Bool -> Defs -> Env Term vars ->
325335
Binder (Closure vars) -> Binder (Closure vars) -> Core Bool
326-
convBinders q i defs env (Pi _ cx ix tx) (Pi _ cy iy ty)
327-
= if cx /= cy
328-
then pure False
329-
else convGen q i defs env tx ty
330-
convBinders q i defs env (Lam _ cx ix tx) (Lam _ cy iy ty)
331-
= if cx /= cy
332-
then pure False
333-
else convGen q i defs env tx ty
334336
convBinders q i defs env bx by
335-
= if multiplicity bx /= multiplicity by
336-
then pure False
337-
else convGen q i defs env (binderType bx) (binderType by)
338-
337+
= if sameBinders bx by && multiplicity bx == multiplicity by
338+
then allM id [ convPiInfo q i defs env (piInfo bx) (piInfo by)
339+
, convGen q i defs env (binderType bx) (binderType by)]
340+
else pure False
341+
where
342+
sameBinders : Binder (Closure vars) -> Binder (Closure vars) -> Bool
343+
sameBinders (Pi {}) (Pi {}) = True
344+
sameBinders (Lam {}) (Lam {}) = True
345+
sameBinders _ _ = False
339346

340347
export
341348
Convert NF where

‎src/Core/Unify.idr‎

Lines changed: 72 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -1047,6 +1047,18 @@ mutual
10471047
unifyBothApps mode loc env xfc fx ax yfc fy ay
10481048
= unifyApp False mode loc env xfc fx ax (NApp yfc fy ay)
10491049

1050+
unifyPiInfo : {auto c : Ref Ctxt Defs} ->
1051+
{auto u : Ref UST UState} ->
1052+
{vars : _} ->
1053+
UnifyInfo -> FC -> Env Term vars ->
1054+
PiInfo (Closure vars) -> PiInfo (Closure vars) ->
1055+
Core (Maybe UnifyResult)
1056+
unifyPiInfo mode loc env Explicit Explicit = pure $ Just success
1057+
unifyPiInfo mode loc env Implicit Implicit = pure $ Just success
1058+
unifyPiInfo mode loc env AutoImplicit AutoImplicit = pure $ Just success
1059+
unifyPiInfo mode loc env (DefImplicit x) (DefImplicit y) = Just <$> unify mode loc env x y
1060+
unifyPiInfo mode loc env _ _ = pure Nothing
1061+
10501062
unifyBothBinders: {auto c : Ref Ctxt Defs} ->
10511063
{auto u : Ref UST UState} ->
10521064
{vars : _} ->
@@ -1058,65 +1070,70 @@ mutual
10581070
Core UnifyResult
10591071
unifyBothBinders mode loc env xfc x (Pi fcx cx ix tx) scx yfc y (Pi fcy cy iy ty) scy
10601072
= do defs <- get Ctxt
1073+
let err = convertError loc env
1074+
(NBind xfc x (Pi fcx cx ix tx) scx)
1075+
(NBind yfc y (Pi fcy cy iy ty) scy)
10611076
if cx /= cy
1062-
then convertError loc env
1063-
(NBind xfc x (Pi fcx cx ix tx) scx)
1064-
(NBind yfc y (Pi fcy cy iy ty) scy)
1065-
else
1066-
do empty <- clearDefs defs
1067-
tx' <- quote empty env tx
1068-
logC "unify.binder" 10 $
1069-
(do ty' <- quote empty env ty
1070-
pure ("Unifying arg types " ++ show tx' ++ " and " ++ show ty'))
1071-
ct <- unify (lower mode) loc env tx ty
1072-
xn <- genVarName "x"
1073-
let env' : Env Term (x :: _)
1074-
= Pi fcy cy Explicit tx' :: env
1075-
case constraints ct of
1076-
[] => -- No constraints, check the scope
1077-
do tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
1078-
tscy <- scy defs (toClosure defaultOpts env (Ref loc Bound xn))
1079-
tmx <- quote empty env tscx
1080-
tmy <- quote empty env tscy
1081-
unify (lower mode) loc env'
1082-
(refsToLocals (Add x xn None) tmx)
1083-
(refsToLocals (Add x xn None) tmy)
1084-
cs => -- Constraints, make new guarded constant
1085-
do txtm <- quote empty env tx
1086-
tytm <- quote empty env ty
1087-
c <- newConstant loc erased env
1088-
(Bind xfc x (Lam fcy cy Explicit txtm) (Local xfc Nothing _ First))
1089-
(Bind xfc x (Pi fcy cy Explicit txtm)
1090-
(weaken tytm)) cs
1091-
tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
1092-
tscy <- scy defs (toClosure defaultOpts env (App loc c (Ref loc Bound xn)))
1093-
tmx <- quote empty env tscx
1094-
tmy <- quote empty env tscy
1095-
cs' <- unify (lower mode) loc env'
1096-
(refsToLocals (Add x xn None) tmx)
1097-
(refsToLocals (Add x xn None) tmy)
1098-
pure (union ct cs')
1077+
then err
1078+
else do Just ci <- unifyPiInfo (lower mode) loc env ix iy
1079+
| Nothing => err
1080+
empty <- clearDefs defs
1081+
tx' <- quote empty env tx
1082+
logC "unify.binder" 10 $
1083+
(do ty' <- quote empty env ty
1084+
pure ("Unifying arg types " ++ show tx' ++ " and " ++ show ty'))
1085+
ct <- unify (lower mode) loc env tx ty
1086+
xn <- genVarName "x"
1087+
let env' : Env Term (x :: _)
1088+
= Pi fcy cy Explicit tx' :: env
1089+
case constraints ct of
1090+
[] => -- No constraints, check the scope
1091+
do tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
1092+
tscy <- scy defs (toClosure defaultOpts env (Ref loc Bound xn))
1093+
tmx <- quote empty env tscx
1094+
tmy <- quote empty env tscy
1095+
cs <- unify (lower mode) loc env'
1096+
(refsToLocals (Add x xn None) tmx)
1097+
(refsToLocals (Add x xn None) tmy)
1098+
pure (union ci cs)
1099+
cs => -- Constraints, make new guarded constant
1100+
do txtm <- quote empty env tx
1101+
tytm <- quote empty env ty
1102+
c <- newConstant loc erased env
1103+
(Bind xfc x (Lam fcy cy Explicit txtm) (Local xfc Nothing _ First))
1104+
(Bind xfc x (Pi fcy cy Explicit txtm)
1105+
(weaken tytm)) cs
1106+
tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
1107+
tscy <- scy defs (toClosure defaultOpts env (App loc c (Ref loc Bound xn)))
1108+
tmx <- quote empty env tscx
1109+
tmy <- quote empty env tscy
1110+
cs' <- unify (lower mode) loc env'
1111+
(refsToLocals (Add x xn None) tmx)
1112+
(refsToLocals (Add x xn None) tmy)
1113+
pure (union ci (union ct cs'))
10991114
unifyBothBinders mode loc env xfc x (Lam fcx cx ix tx) scx yfc y (Lam fcy cy iy ty) scy
11001115
= do defs <- get Ctxt
1116+
let err = convertError loc env
1117+
(NBind xfc x (Lam fcx cx ix tx) scx)
1118+
(NBind yfc y (Lam fcy cy iy ty) scy)
11011119
if cx /= cy
1102-
then convertError loc env
1103-
(NBind xfc x (Lam fcx cx ix tx) scx)
1104-
(NBind yfc y (Lam fcy cy iy ty) scy)
1105-
else
1106-
do empty <- clearDefs defs
1107-
ct <- unify (lower mode) loc env tx ty
1108-
xn <- genVarName "x"
1109-
txtm <- quote empty env tx
1110-
let env' : Env Term (x :: _)
1111-
= Lam fcx cx Explicit txtm :: env
1112-
1113-
tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
1114-
tscy <- scy defs (toClosure defaultOpts env (Ref loc Bound xn))
1115-
tmx <- quote empty env tscx
1116-
tmy <- quote empty env tscy
1117-
cs' <- unify (lower mode) loc env' (refsToLocals (Add x xn None) tmx)
1118-
(refsToLocals (Add x xn None) tmy)
1119-
pure (union ct cs')
1120+
then err
1121+
else do empty <- clearDefs defs
1122+
Just ci <- unifyPiInfo (lower mode) loc env ix iy
1123+
| Nothing => err
1124+
ct <- unify (lower mode) loc env tx ty
1125+
xn <- genVarName "x"
1126+
txtm <- quote empty env tx
1127+
let env' : Env Term (x :: _)
1128+
= Lam fcx cx Explicit txtm :: env
1129+
1130+
tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn))
1131+
tscy <- scy defs (toClosure defaultOpts env (Ref loc Bound xn))
1132+
tmx <- quote empty env tscx
1133+
tmy <- quote empty env tscy
1134+
cs' <- unify (lower mode) loc env' (refsToLocals (Add x xn None) tmx)
1135+
(refsToLocals (Add x xn None) tmy)
1136+
pure (union ci (union ct cs'))
11201137

11211138
unifyBothBinders mode loc env xfc x bx scx yfc y by scy
11221139
= convertError loc env

‎src/TTImp/ProcessData.idr‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -506,7 +506,7 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o
506506
if ok then pure (mw, vis, tot, fullty)
507507
else do logTermNF "declare.data" 1 "Previous" [] (type ndef)
508508
logTermNF "declare.data" 1 "Now" [] fullty
509-
throw (AlreadyDefined fc n)
509+
throw (CantConvert fc (gamma defs) [] (type ndef) fullty)
510510
_ => throw (AlreadyDefined fc n)
511511

512512
logTermNF "declare.data" 5 ("data " ++ show n) [] fullty

‎tests/idris2/basic/basic073/DefaultHole.idr‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
foo : (Nat -> {default 42 _ : Nat} -> Nat) -> Nat
2+
foo f = f 0
3+
4+
bar : Nat
5+
bar = foo baz
6+
where
7+
baz : Nat -> {default ? y : Nat} -> Nat
8+
baz x = x + y

‎tests/idris2/basic/basic073/expected‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
1/1: Building DefaultHole (DefaultHole.idr)

‎tests/idris2/basic/basic073/run‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
. ../../../testutils.sh
2+
3+
check DefaultHole.idr

‎tests/idris2/data/data006/ConvertPiInfo.idr‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
--------------
2+
-- Explicit --
3+
--------------
4+
5+
data EI : Type -> Type
6+
data EI : {_ : Type} -> Type where
7+
8+
data EA : Type -> Type
9+
data EA : {auto _ : Type} -> Type where
10+
11+
data ED : Type -> Type
12+
data ED : {default Int _ : Type} -> Type where
13+
14+
--------------
15+
-- Implicit --
16+
--------------
17+
18+
data IE : {_ : Type} -> Type
19+
data IE : Type -> Type where
20+
21+
data IA : {_ : Type} -> Type
22+
data IA : {auto _ : Type} -> Type where
23+
24+
data ID : {_ : Type} -> Type
25+
data ID : {default Int _ : Type} -> Type where
26+
27+
----------
28+
-- Auto --
29+
----------
30+
31+
data AE : {auto _ : Type} -> Type
32+
data AE : Type -> Type where
33+
34+
data AI : {auto _ : Type} -> Type
35+
data AI : {_ : Type} -> Type where
36+
37+
data AD : {auto _ : Type} -> Type
38+
data AD : {default Int _ : Type} -> Type where
39+
40+
-------------
41+
-- Default --
42+
-------------
43+
44+
data DE : {default Int _ : Type} -> Type
45+
data DE : Type -> Type where
46+
47+
data DI : {default Int _ : Type} -> Type
48+
data DI : {_ : Type} -> Type where
49+
50+
data DA : {default Int _ : Type} -> Type
51+
data DA : {auto _ : Type} -> Type where

‎tests/idris2/data/data006/expected‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
1/1: Building ConvertPiInfo (ConvertPiInfo.idr)
2+
Error: Mismatch between: Type -> Type and Type.
3+
4+
ConvertPiInfo:6:1--6:35
5+
2 | -- Explicit --
6+
3 | --------------
7+
4 |
8+
5 | data EI : Type -> Type
9+
6 | data EI : {_ : Type} -> Type where
10+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
11+
12+
Error: Mismatch between: Type -> Type and Type => Type.
13+
14+
ConvertPiInfo:9:1--9:40
15+
5 | data EI : Type -> Type
16+
6 | data EI : {_ : Type} -> Type where
17+
7 |
18+
8 | data EA : Type -> Type
19+
9 | data EA : {auto _ : Type} -> Type where
20+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
21+
22+
Error: Mismatch between: Type -> Type and {default Int _ : Type} -> Type.
23+
24+
ConvertPiInfo:12:1--12:47
25+
08 | data EA : Type -> Type
26+
09 | data EA : {auto _ : Type} -> Type where
27+
10 |
28+
11 | data ED : Type -> Type
29+
12 | data ED : {default Int _ : Type} -> Type where
30+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
31+
32+
Error: Mismatch between: Type and Type -> Type.
33+
34+
ConvertPiInfo:19:1--19:29
35+
15 | -- Implicit --
36+
16 | --------------
37+
17 |
38+
18 | data IE : {_ : Type} -> Type
39+
19 | data IE : Type -> Type where
40+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
41+
42+
Error: Mismatch between: Type and Type => Type.
43+
44+
ConvertPiInfo:22:1--22:40
45+
18 | data IE : {_ : Type} -> Type
46+
19 | data IE : Type -> Type where
47+
20 |
48+
21 | data IA : {_ : Type} -> Type
49+
22 | data IA : {auto _ : Type} -> Type where
50+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
51+
52+
Error: Mismatch between: Type and {default Int _ : Type} -> Type.
53+
54+
ConvertPiInfo:25:1--25:47
55+
21 | data IA : {_ : Type} -> Type
56+
22 | data IA : {auto _ : Type} -> Type where
57+
23 |
58+
24 | data ID : {_ : Type} -> Type
59+
25 | data ID : {default Int _ : Type} -> Type where
60+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
61+
62+
Error: Mismatch between: Type => Type and Type -> Type.
63+
64+
ConvertPiInfo:32:1--32:29
65+
28 | -- Auto --
66+
29 | ----------
67+
30 |
68+
31 | data AE : {auto _ : Type} -> Type
69+
32 | data AE : Type -> Type where
70+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
71+
72+
Error: Mismatch between: Type => Type and Type.
73+
74+
ConvertPiInfo:35:1--35:35
75+
31 | data AE : {auto _ : Type} -> Type
76+
32 | data AE : Type -> Type where
77+
33 |
78+
34 | data AI : {auto _ : Type} -> Type
79+
35 | data AI : {_ : Type} -> Type where
80+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
81+
82+
Error: Mismatch between: Type => Type and {default Int _ : Type} -> Type.
83+
84+
ConvertPiInfo:38:1--38:47
85+
34 | data AI : {auto _ : Type} -> Type
86+
35 | data AI : {_ : Type} -> Type where
87+
36 |
88+
37 | data AD : {auto _ : Type} -> Type
89+
38 | data AD : {default Int _ : Type} -> Type where
90+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
91+
92+
Error: Mismatch between: {default Int _ : Type} -> Type and Type -> Type.
93+
94+
ConvertPiInfo:45:1--45:29
95+
41 | -- Default --
96+
42 | -------------
97+
43 |
98+
44 | data DE : {default Int _ : Type} -> Type
99+
45 | data DE : Type -> Type where
100+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
101+
102+
Error: Mismatch between: {default Int _ : Type} -> Type and Type.
103+
104+
ConvertPiInfo:48:1--48:35
105+
44 | data DE : {default Int _ : Type} -> Type
106+
45 | data DE : Type -> Type where
107+
46 |
108+
47 | data DI : {default Int _ : Type} -> Type
109+
48 | data DI : {_ : Type} -> Type where
110+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
111+
112+
Error: Mismatch between: {default Int _ : Type} -> Type and Type => Type.
113+
114+
ConvertPiInfo:51:1--51:40
115+
47 | data DI : {default Int _ : Type} -> Type
116+
48 | data DI : {_ : Type} -> Type where
117+
49 |
118+
50 | data DA : {default Int _ : Type} -> Type
119+
51 | data DA : {auto _ : Type} -> Type where
120+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
121+

‎tests/idris2/data/data006/run‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
. ../../../testutils.sh
2+
3+
check ConvertPiInfo.idr

0 commit comments

Comments
 (0)