[ fix ] Support matching on Type in impossible cases

Author: spcfox

src/TTImp/Impossible.idr

@@ -193,8 +193,9 @@ mutual
       go (IMustUnify fc r tm) exps autos named
         = Erased fc . Dotted <$> go tm exps autos named
       go (IPrimVal fc c) _ _ _ = pure (PrimVal fc c)
-      -- We're taking UniqueDefault here, _and_ we're falling through to nextVar otherwise, which is sketchy.
-      -- On option is to try each and emit an AmbiguousElab?  We maybe should respect `UniqueDefault` if there
+      go (IType fc) _ _ _ = pure (TType fc $ MN "top" 0)
+      -- We're taking UniqueDefault here, _and_ we're falling through to error otherwise, which is sketchy.
+      -- One option is to try each and emit an AmbiguousElab? We maybe should respect `UniqueDefault` if there
       -- is no evidence (mty), but we should _try_ to resolve here if there is an mty.
       go (IAlternative _ (UniqueDefault tm) _) exps autos named
         = go tm exps autos named

tests/idris2/coverage/coverage029/expected

@@ -1,13 +1,4 @@
 1/1: Building Main (Main.idr)
-Warning: Main:4:11--4:15:Unsupported term in impossible clause: Type
-
-Main:4:11--4:15
- 1 | import Language.Reflection
- 2 | 
- 3 | matchType : Bool -> Void
- 4 | matchType Type impossible
-               ^^^^
-
 Warning: Main:7:12--7:20:Unsupported term in impossible clause: `((fromInteger 1 + fromInteger 1))
 
 Main:7:12--7:20
@@ -165,7 +156,7 @@ Main:3:1--3:25
      ^^^^^^^^^^^^^^^^^^^^^^^^
 
 Missing cases:
-    matchType _
+    matchType True
 
 Error: matchWith is not covering.
 

tests/idris2/coverage/coverage032/Main.idr

@@ -0,0 +1,8 @@
+%default total
+
+data X : Type -> Type where
+  MkX : (a : Type) -> X a
+
+f : X Nat -> ()
+f (MkX Type) impossible
+f (MkX Nat) = ()

tests/idris2/coverage/coverage032/expected

@@ -0,0 +1 @@
+1/1: Building Main (Main.idr)

tests/idris2/coverage/coverage032/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Main.idr