Look for scrutinee type in case

We can work out what it should be since each case is supposed to have
the same type, so we can look ahead to the alternatives. This way, we
don't have to rely on the scrutinee alone to calculate the type of the
case block. (Idris 1 does this too but I've only just encountered the
need for it in Idris 2 now!)

docs/typedd/typedd.rst

@@ -11,6 +11,11 @@ code is also [going to be] part of the test suite (see `tests/typedd-book
 <https://github.com/edwinb/Idris2/tree/master/tests/typedd-book>`_ in the Idris
 2 source).
 
+If you are new to Idris, and learning from the book, we recommend working
+through the first 3-4 chapters with Idris 1, to avoid the need to worry about
+the changes described here. After that, refer to this document for any
+necessary changes.
+
 Chapter 1
 ---------
 

src/TTImp/Elab/Case.idr

@@ -311,9 +311,12 @@ checkCase : {vars : _} ->
             FC -> (scr : RawImp) -> (ty : RawImp) -> List ImpClause ->
             Maybe (Glued vars) ->
             Core (Term vars, Glued vars)
-checkCase rig elabinfo nest env fc scr scrty_exp alts exp
+checkCase rig elabinfo nest env fc scr scrty_in alts exp
     = delayElab fc rig env exp $
-        do (scrtyv, scrtyt) <- check Rig0 elabinfo nest env scrty_exp
+        do scrty_exp <- case scrty_in of
+                             Implicit _ _ => guessScrType alts
+                             _ => pure scrty_in
+           (scrtyv, scrtyt) <- check Rig0 elabinfo nest env scrty_exp
                                      (Just (gType fc))
            logTerm 10 "Expected scrutinee type" scrtyv
            -- Try checking at the given multiplicity; if that doesn't work,
@@ -347,3 +350,38 @@ checkCase rig elabinfo nest env fc scr scrty_exp alts exp
     checkConcrete (NApp _ (NMeta n i _) _)
         = throw (GenericMsg (getFC scr) "Can't infer type for case scrutinee")
     checkConcrete _ = pure ()
+
+    applyTo : Defs -> RawImp -> NF [] -> Core RawImp
+    applyTo defs ty (NBind fc _ (Pi _ Explicit _) sc)
+        = applyTo defs (IApp fc ty (Implicit fc False))
+               !(sc defs (toClosure defaultOpts [] (Erased fc False)))
+    applyTo defs ty (NBind _ x (Pi _ _ _) sc)
+        = applyTo defs (IImplicitApp fc ty (Just x) (Implicit fc False))
+               !(sc defs (toClosure defaultOpts [] (Erased fc False)))
+    applyTo defs ty _ = pure ty
+
+    -- Get the name and type of the family the scrutinee is in
+    getRetTy : Defs -> NF [] -> Core (Maybe (Name, NF []))
+    getRetTy defs (NBind fc _ (Pi _ _ _) sc)
+        = getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc False)))
+    getRetTy defs (NTCon _ n _ arity _)
+        = do Just ty <- lookupTyExact n (gamma defs)
+                  | Nothing => pure Nothing
+             pure (Just (n, !(nf defs [] ty)))
+    getRetTy _ _ = pure Nothing
+
+    -- Guess a scrutinee type by looking at the alternatives, so that we
+    -- have a hint for building the case type
+    guessScrType : List ImpClause -> Core RawImp
+    guessScrType [] = pure $ Implicit fc False
+    guessScrType (PatClause _ x _ :: xs)
+        = case getFn x of
+               IVar _ n =>
+                  do defs <- get Ctxt
+                     [(n', (_, ty))] <- lookupTyName n (gamma defs)
+                         | _ => guessScrType xs
+                     Just (tyn, tyty) <- getRetTy defs !(nf defs [] ty)
+                         | _ => guessScrType xs
+                     applyTo defs (IVar fc tyn) tyty
+               _ => guessScrType xs
+    guessScrType (_ :: xs) = guessScrType xs

tests/idris2/basic030/expected

@@ -1,3 +1,7 @@
 1/1: Building arity (arity.idr)
-arity.idr:5:16--5:22:While processing right hand side of foo at arity.idr:4:1--7:1:
-Constructor Main.MkN is not fully applied
+arity.idr:4:16--4:22:While processing right hand side of foo at arity.idr:4:1--7:1:
+When unifying (1 {arg:169} : Nat) -> MyN and MyN
+Mismatch between:
+	(1 {arg:169} : Nat) -> MyN
+and
+	MyN

tests/ttimp/qtt002/expected

@@ -1,6 +1,6 @@
 Processing as TTImp
 Written TTC
 Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:19} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just y a (%pi Rig0 Explicit Just ws ((Main.Vect {k:19}) a) (%pi Rig1 Explicit Just zs ((Main.Vect (Main.S {k:19})) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S (Main.S {k:19}))) m)) a))))))))))
-Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:48} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect {k:48}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:48})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:48})) m)) a)))))))))
-Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:78} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just zs ((Main.Vect {k:78}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:78})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:78}) a) ((Main.Vect ((Main.plus (Main.S {k:78})) m)) a))))))))))
+Yaffle> Main.bar : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:49} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig1 Explicit Just zs ((Main.Vect {k:49}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:49})) a) (%pi Rig0 Explicit Just n Main.Nat ((Main.Vect ((Main.plus (Main.S {k:49})) m)) a)))))))))
+Yaffle> Main.baz : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just {k:80} Main.Nat (%pi RigW Explicit Nothing a (%pi Rig0 Explicit Just zs ((Main.Vect {k:80}) a) (%pi Rig0 Explicit Just xs ((Main.Vect (Main.S {k:80})) a) (%pi Rig0 Explicit Just n Main.Nat (%pi Rig1 Explicit Just ts ((Main.Vect {k:80}) a) ((Main.Vect ((Main.plus (Main.S {k:80})) m)) a))))))))))
 Yaffle> Bye for now!