Unsolved metas are errors

TODO.md

@@ -1,9 +1,20 @@
 
 ## TODO
 
+- [x] Unsolved metas should be errors (user metas are fine)
+- [x] Better syntax for forward declared data (so we can distinguish from functions)
+- [ ] maybe allow "Main" module name for any file
+- [ ] Improve handling of names:
+  - We need FC on names in a lot of places
+  - [ ] FC for duplicate data constructor name is wrong (points to `data`)
+  - [ ] FC on bad import should point to the name
+  - [x] Current module overrides imports
+  - [ ] Allow Qualified names in surface syntax
+  - Don't disambiguate on type for now
 - [x] change "in prefix position" and "trailing operator" errors to do sections
 - [ ] maybe add fat arrows, I keep wanting to type them, `{{...}}` is a little ugly
-  - There may be ambiguity issues at the parsing level, but we don't have typecase, so...
+  - There may be ambiguity issues at the parsing level, but we don't have typecase, so.
+  - It's less to type, too.
 - [x] get some names on add missing cases (if not too difficult)
 - [ ] Implement "add missing cases" for playground
 - [x] add optional types to case `case xxx : Maybe Int of ...`
@@ -53,6 +64,7 @@
 - [ ] See if we can split up `Elab.newt`
   - Unify, checking, and case builder have circular references.
   - Perhaps unify should return constraints instead of calling solve directly.
+  - passing a pointer to `check` in the context may suffice
 - [ ] Add error for non-linear names in pattern matching (currently it picks one)
   - We probably should handle forced values. Idris requires them to have the same name.
 - [ ] Functions with erased-only arguments still get called with `()` - do we want this or should they be constants?
@@ -82,6 +94,7 @@
 - [ ] Look into descriptions, etc.
   - Can generating descriptions help with automatic "show" implementations
   - We lost debug printing when switching to numeric tags
+  - Where did I see the idea of generating descriptions for inductive types?
 - [ ] Add info to Ref/VRef (is dcon, arity, etc)
   - To save lookups during compilation and it might make eval faster
 - [x] number tags for data constructors

src/Lib/ProcessDecl.newt

@@ -69,7 +69,8 @@ logMetas (Unsolved fc k ctx ty kind cons :: rest) = do
           pure ("  \{show $ length' matches} Solutions: \{show matches}" :: Nil)
 
         _ => pure Nil
-      info fc $ unlines ((msg :: Nil) ++ msgs ++ sols)
+      -- info fc $ unlines ((msg :: Nil) ++ msgs ++ sols)
+      addError $ E fc $ unlines ((msg :: Nil) ++ msgs ++ sols)
       logMetas rest
 
 

tests/TestCase5.newt

@@ -1,35 +0,0 @@
-module TestCase5
-
--- last bit tests pulling solutions from context
-
-data Plus : U -> U where
-    MkPlus : {A : U} -> (A -> A -> A) -> Plus A
-
-infixl 7 _+_
-_+_ : {A : U} {{_ : Plus A}} -> A -> A -> A
-_+_ {{MkPlus plus}} x y = plus x y
-
-
-pfunc plusInt : Int -> Int -> Int := `(x,y) => x + y`
-
-PlusInt : Plus Int
-PlusInt = MkPlus plusInt
-
--- TODO this needs some aggressive inlining...
-double : Int -> Int
-double x = x + x
-
-data Nat : U where
-    Z : Nat
-    S : Nat -> Nat
-
-plus : Nat -> Nat -> Nat
-plus Z m = m
-plus (S n) m = S (plus n m)
-
-PlusNat : Plus Nat
-PlusNat = MkPlus plus
-
-double2 : {A : U} {{foo : Plus A}} -> A -> A
-double2 = \ a => a + a
-

tests/TypeClass.newt

@@ -1,84 +0,0 @@
-module TypeClass
-
-data Monad : (U -> U) -> U where
-  MkMonad : { M : U -> U } ->
-            (bind : ∀ A B. (M A) -> (A -> M B) -> M B) ->
-            (pure : ∀ A. A -> M A) ->
-            Monad M
-
-infixl 1 _>>=_ _>>_
-_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b
-_>>=_ {{MkMonad bind' _}}  ma amb = bind' ma amb
-
-_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
-ma >> mb = mb
-
-pure : ∀ m a. {{Monad m}} -> a -> m a
-pure {{MkMonad _ pure'}} a = pure' a
-
-data Either : U -> U -> U where
-  Left : ∀ A B. A -> Either A B
-  Right : ∀ A B. B -> Either A B
-
-bindEither : ∀ A B C. (Either A B) -> (B -> Either A C) -> Either A C
-bindEither (Left a) amb = Left a
-bindEither (Right b) amb = amb b
-
-EitherMonad : {A : U} -> Monad (Either A)
-EitherMonad = MkMonad {Either A} bindEither Right
-
-data Maybe : U -> U where
-  Just    : ∀ A. A -> Maybe A
-  Nothing : ∀ A. Maybe A
-
-bindMaybe : ∀ A B. Maybe A -> (A -> Maybe B) -> Maybe B
-bindMaybe Nothing amb = Nothing
-bindMaybe (Just a) amb = amb a
-
-MaybeMonad : Monad Maybe
-MaybeMonad = MkMonad bindMaybe Just
-
-infixr 7 _::_
-data List : U -> U where
-  Nil : ∀ A. List A
-  _::_ : ∀ A. A -> List A -> List A
-
-infixl 7 _++_
-_++_ : ∀ A. List A -> List A -> List A
-Nil ++ ys = ys
-(x :: xs) ++ ys = x :: (xs ++ ys)
-
-bindList : ∀ A B. List A -> (A -> List B) -> List B
-bindList Nil f = Nil
-bindList (x :: xs) f = f x ++ bindList xs f
-
-singleton : ∀ A. A -> List A
-singleton a = a :: Nil
-
--- TODO need better error when the monad is not defined
-ListMonad : Monad List
-ListMonad = MkMonad bindList singleton
-
-infixr 1 _,_
-data Pair : U -> U -> U where
-  _,_ : ∀ A B. A -> B -> Pair A B
-
-
-
-test : Maybe Int
-test = pure 10
-
-foo : Int -> Maybe Int
-foo x = Just 42 >> Just x >>= (\ x => pure 10)
-
-bar : Int -> Maybe Int
-bar x = do
-  let y = x
-  z <- Just x
-  pure z
-
-baz : ∀ A B. List A -> List B -> List (Pair A B)
-baz xs ys = do
-  x <- xs
-  y <- ys
-  pure (x , y)