git.iko.soy/Idris-dev
on master help sign in
x = y now tries homogeneous equality first

People often assume that the type of x is enough to give the type of y, but because = is heterogeneous this isn't always the case. So now the elaborator will assume homogeneous equality is intended, and revert to heterogeneous when necessary. Fixes #1386

commit4d62d30aac42723f71a20fd97f1478edca2821d2 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 15 Jul 2014, 18:46 (12 years ago) parent228877a
2 files changed+27
compare with master
unifiedsplit
libs/prelude/Builtins.idr+8 src/Idris/ElabTerm.hs+19
libs/prelude/Builtins.idr+8
@@ -15,6 +15,14 @@ FalseElim : _|_ -> a
1515||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
1616data Symbol_ : String -> Type where
1717
18+-- Eq_ : a -> a -> Type
19+-- Eq_ x y = (=) _ _ x y
20+
21+infix 5 ~=~
22+
23+(~=~) : a -> b -> Type
24+(~=~) x y = (=) _ _ x y
25+
1826-- ------------------------------------------------------ [ For rewrite tactic ]
1927||| Perform substitution in a term according to some equality.
2028|||
src/Idris/ElabTerm.hs+19
@@ -250,6 +250,25 @@ elab ist info emode opts fn tm
250250 elab' ina (PRefl fc t)
251251 = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
252252 pimp (sMN 0 "x") t False])
253+ elab' ina (PEq fc Placeholder Placeholder l r)
254+ = try (do tyn <- getNameFrom (sMN 0 "aqty")
255+ claim tyn RType
256+ movelast tyn
257+ elab' ina (PApp fc (PRef fc eqTy)
258+ [pimp (sUN "A") (PRef fc tyn) True,
259+ pimp (sUN "B") (PRef fc tyn) False,
260+ pexp l, pexp r]))
261+ (do atyn <- getNameFrom (sMN 0 "aqty")
262+ btyn <- getNameFrom (sMN 0 "bqty")
263+ claim atyn RType
264+ movelast atyn
265+ claim btyn RType
266+ movelast btyn
267+ elab' ina (PApp fc (PRef fc eqTy)
268+ [pimp (sUN "A") (PRef fc atyn) True,
269+ pimp (sUN "B") (PRef fc btyn) False,
270+ pexp l, pexp r]))
271+
253272 elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)
254273 [pimp (sUN "A") lt True,
255274 pimp (sUN "B") rt False,