git.iko.soy/Idris-dev
on master help sign in
Type class resolution fix (disables Decidable.Decidable)

Instances should not be resolved when there is no information available. Previously, resolution just guessed at an instance in this case, though this was never intended behaviour!

commite8c2badae269e7171dbd8e64c6af17455a1e89f5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 15 Jun 2013, 00:10 (13 years ago) parent7bfa10c
4 files changed+24−3
compare with master
unifiedsplit
idris.cabal+1−1 lib/Decidable/Decidable.idr+6−1 lib/Decidable/Order.idr+8 src/Idris/ElabTerm.hs+9−1
idris.cabal+1−1
@@ -1,5 +1,5 @@
11Name: idris
2−Version: 0.9.8
2+Version: 0.9.8.1
33License: BSD3
44License-file: LICENSE
55Author: Edwin Brady
lib/Decidable/Decidable.idr+6−1
@@ -6,6 +6,11 @@ module Decidable.Decidable
66-- Typeclass for decidable n-ary Relations
77--------------------------------------------------------------------------------
88
9+{-
10+This can't work yet! The class parameters must appear in the method type
11+signatures otherwise when defining the instances class resolution doesn't
12+have any clues...
13+
914using (t : Type)
1015 class Rel (p : t) where
1116 total liftRel : (Type -> Type) -> Type
@@ -16,4 +21,4 @@ using (t : Type)
1621using (P : Type, p : P)
1722 data Given : Dec P -> Type where
1823 always : Given (Yes p)
19−
24+-}
lib/Decidable/Order.idr+8
@@ -1,5 +1,10 @@
11module Decidable.Order
22
3+%access public
4+
5+{-
6+Doesn't work yet, see note in Decidable.idr
7+
38import Decidable.Decidable
49import Decidable.Equality
510
@@ -77,3 +82,6 @@ instance Decidable NatLTE where
7782
7883lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
7984lte m n = decide {p = NatLTE} m n
85+
86+-}
87+
src/Idris/ElabTerm.hs+9−1
@@ -615,9 +615,11 @@ resolveTC depth fn ist
615615 if True -- all (\n -> not (n `elem` hs)) (freeNames g)
616616 then try' (trivial ist)
617617 (do t <- goal
618− let insts = findInstances ist t
619618 let (tc, ttypes) = unApply t
620619 scopeOnly <- needsDefault t tc ttypes
620+ let insts_in = findInstances ist t
621+ let insts = if scopeOnly then filter chaser insts_in
622+ else insts_in
621623 tm <- get_term
622624-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
623625-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
@@ -633,6 +635,12 @@ resolveTC depth fn ist
633635 elabTC n | n /= fn && tcname n = (resolve n depth, show n)
634636 | otherwise = (fail "Can't resolve", show n)
635637
638+ -- HACK! Rather than giving a special name, better to have some kind
639+ -- of flag in ClassInfo structure
640+ chaser (UN ('@':'@':_)) = True
641+ chaser (NS n _) = chaser n
642+ chaser _ = False
643+
636644 needsDefault t num@(P _ (NS (UN "Num") ["Builtins"]) _) [P Bound a _]
637645 = do focus a
638646 fill (RConstant IType) -- default Int