Fix loading of hints, and add test

Need to add by full name, due to ordering of loading (the name it's
attached to may not be resolved yet!). This doesn't seem to cause any
performance problems but we can revisit if it does.

src/Core/Binary.idr

@@ -359,7 +359,6 @@ readFromTTC loc reexp fname modNS importAs
          setNS (currentNS ttc)
          -- Set up typeHints and autoHints based on the loaded data
          traverse_ (addTypeHint loc) (typeHints ttc)
-         defs <- get Ctxt
          traverse_ addAutoHint (autoHints ttc)
          -- Set up pair/rewrite etc names
          updatePair (pairnames ttc)

src/Core/Context.idr

@@ -1090,7 +1090,7 @@ getSearchData fc defaults target
     = do defs <- get Ctxt
          Just (TCon _ _ _ dets _ _) <- lookupDefExact target (gamma defs)
               | _ => throw (UndefinedName fc target)
-         let hs = case lookup target (typeHints defs) of
+         let hs = case lookup !(toFullNames target) (typeHints defs) of
                        Just hs => hs
                        Nothing => []
          if defaults
@@ -1166,7 +1166,10 @@ addHintFor : {auto c : Ref Ctxt Defs} ->
 					   FC -> Name -> Name -> Bool -> Bool -> Core ()
 addHintFor fc tyn_in hintn_in direct loading
     = do defs <- get Ctxt
-         tyn <- toResolvedNames tyn_in
+         tyn <- toFullNames tyn_in
+          -- ^ We have to index by full name because of the order we load -
+          -- the name may not be resolved yet when we load the hints.
+          -- Revisit if this turns out to be a bottleneck (it seems unlikely)
          hintn <- toResolvedNames hintn_in
 
          let hs = case lookup tyn (typeHints defs) of

tests/Main.idr

@@ -26,7 +26,7 @@ idrisTests
     = ["basic001", "basic002", "basic003", "basic004", "basic005",
        "basic006", "basic007", "basic008", "basic009", "basic010",
        "basic011", "basic012", "basic013", "basic014", "basic015",
-       "basic016", "basic017", "basic018", "basic019",
+       "basic016", "basic017", "basic018", "basic019", "basic020",
        "coverage001", "coverage002", "coverage003", "coverage004",
        "error001", "error002", "error003", "error004", "error005",
        "error006",

tests/idris2/basic020/Mut.idr

@@ -0,0 +1,44 @@
+mutual
+  data MyBool = MyFalse | MyTrue
+
+  even : Nat -> MyBool
+  even (S k) = odd k
+  even Z = MyTrue
+
+  odd : Nat -> MyBool
+  odd (S k) = even k
+  odd Z = MyFalse
+
+eodd : Nat -> (Bool, Bool)
+eodd num = (isEven num, isOdd num)
+  where
+    mutual
+      isEven : Nat -> Bool
+      isEven (S k) = isOdd k
+      isEven Z = True
+
+      isOdd : Nat -> Bool
+      isOdd (S k) = isEven k
+      isOdd Z = False
+
+data Box : Type -> Type where
+     MkBox : a -> Box a
+
+mutual
+  Functor Box where
+    map f b 
+        = do b' <- b
+             pure (f b')
+
+  Applicative Box where
+    (<*>) f a 
+        = do f' <- f
+             a' <- a
+             pure (f' a')
+    pure = MkBox
+
+  Monad Box where
+    (>>=) (MkBox val) k = k val
+
+boxy : Box Integer
+boxy = map (*2) (MkBox 20)

tests/idris2/basic020/expected

@@ -0,0 +1,9 @@
+1/1: Building Mut (Mut.idr)
+Welcome to Idris 2 version 0.0. Enjoy yourself!
+Main> MyTrue
+Main> MyFalse
+Main> (True, False)
+Main> (False, True)
+Main> MkBox 40
+Main> MkBox 20
+Main> Bye for now!

tests/idris2/basic020/input

@@ -0,0 +1,7 @@
+even 4
+odd 4
+eodd 4
+eodd 5
+boxy
+map (*2) (MkBox 10)
+:q

tests/idris2/basic020/run

@@ -0,0 +1,3 @@
+$1 Mut.idr < input
+
+rm -rf build