git.iko.soy/Idris-dev
on master help sign in
Fix DecEq implementation on primitives

We can't just make up any old proof for the not equal case, since it messes up type checking later! Instead, use a postulate, since we won't do any calculation with it since it produces a Void.

commit3b35e39eb964396f6ff0aaf313007cebc45fd7c4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 26 May 2018, 17:03 (8 years ago) parent88f5c71
1 file changed+8−13
compare with master
unifiedsplit
libs/prelude/Decidable/Equality.idr+8−13
libs/prelude/Decidable/Equality.idr+8−13
@@ -157,7 +157,8 @@ implementation DecEq a => DecEq (List a) where
157157
158158
159159-- For the primitives, we have to cheat because we don't have access to their
160−-- internal implementations.
160+-- internal implementations. We postulate the inequality proofs because we're
161+-- never going to have to compute anything from them.
161162
162163--------------------------------------------------------------------------------
163164-- Int
@@ -169,8 +170,7 @@ implementation DecEq Int where
169170 False => No primitiveNotEq
170171 where primitiveEq : x = y
171172 primitiveEq = really_believe_me (Refl {x})
172− primitiveNotEq : x = y -> Void
173− primitiveNotEq = really_believe_me (id {a = x = y})
173+ postulate primitiveNotEq : x = y -> Void
174174
175175--------------------------------------------------------------------------------
176176-- Char
@@ -182,8 +182,7 @@ implementation DecEq Char where
182182 False => No primitiveNotEq
183183 where primitiveEq : x = y
184184 primitiveEq = really_believe_me (Refl {x})
185− primitiveNotEq : x = y -> Void
186− primitiveNotEq = really_believe_me (id {a = x = y})
185+ postulate primitiveNotEq : x = y -> Void
187186
188187--------------------------------------------------------------------------------
189188-- Integer
@@ -195,8 +194,7 @@ implementation DecEq Integer where
195194 False => No primitiveNotEq
196195 where primitiveEq : x = y
197196 primitiveEq = really_believe_me (Refl {x})
198− primitiveNotEq : x = y -> Void
199− primitiveNotEq = really_believe_me (id {a = x = y})
197+ postulate primitiveNotEq : x = y -> Void
200198
201199--------------------------------------------------------------------------------
202200-- String
@@ -208,8 +206,7 @@ implementation DecEq String where
208206 False => No primitiveNotEq
209207 where primitiveEq : x = y
210208 primitiveEq = really_believe_me (Refl {x})
211− primitiveNotEq : x = y -> Void
212− primitiveNotEq = really_believe_me (id {a = x = y})
209+ postulate primitiveNotEq : x = y -> Void
213210
214211--------------------------------------------------------------------------------
215212-- Ptr
@@ -221,8 +218,7 @@ implementation DecEq Ptr where
221218 False => No primitiveNotEq
222219 where primitiveEq : x = y
223220 primitiveEq = really_believe_me (Refl {x})
224− primitiveNotEq : x = y -> Void
225− primitiveNotEq = really_believe_me (id {a = x = y})
221+ postulate primitiveNotEq : x = y -> Void
226222
227223--------------------------------------------------------------------------------
228224-- ManagedPtr
@@ -234,5 +230,4 @@ implementation DecEq ManagedPtr where
234230 False => No primitiveNotEq
235231 where primitiveEq : x = y
236232 primitiveEq = really_believe_me (Refl {x})
237− primitiveNotEq : x = y -> Void
238− primitiveNotEq = really_believe_me (id {a = x = y})
233+ postulate primitiveNotEq : x = y -> Void