Fix some issues with error reporting

src/Types/Holes.hs

@@ -351,7 +351,10 @@ genNameWithHint vars ty =
     discriminate _ = undefined
 
 nonRec :: Var Typed -> Type Typed -> Bool
-nonRec v (TyApps (TyCon x ()) _) = x /= v
+nonRec v (TyApps c _) =
+  case c of
+    TyCon x _ -> x /= v
+    _ -> True
 nonRec v (TyTuple a b) = nonRec v a && nonRec v b
 nonRec v (TyPi _ b) = nonRec v b
 nonRec _ TyVar{} = True
@@ -363,4 +366,4 @@ nonRec v (TyRows t xs) = nonRec v t && all (nonRec v . snd) xs
 nonRec v (TyExactRows xs) = all (nonRec v . snd) xs
 nonRec v (TyParens p) = nonRec v p
 nonRec v (TyOperator l o r) = nonRec v o && nonRec v l && nonRec v r
-nonRec _ _ = error "nonRec: that's a weird type you have there."
+nonRec _ t = error $ "nonRec: unhandled type " ++ show t

src/Types/Infer.hs

@@ -173,6 +173,38 @@ check ex@(ListExp es an) t@(TyApp f x) | f == tyList = do
 
   pure (ExprWrapper w (buildList an x es) (an, t))
 
+check ex@(MLet bindv pat expr body an) wanted = do
+  let reason = becauseExp ex
+      bind = VarRef bindv an
+      bind :: Expr Desugared
+  (bind, bind_t) <- infer bind
+
+  ~(Anon action_t, c1, w1) <- quantifier reason (/= Req) bind_t
+  expr <- check expr action_t
+
+  ~(Anon cont_t, res, w2)    <- quantifier reason (/= Req) c1
+  cont_a <- freshTV
+  w3 <- subsumes reason (cont_a :-> wanted) cont_t
+
+  (pat', ms, cs, is) <- checkPattern pat cont_a
+  let tvs = boundTvs pat' ms
+
+  body <- implies (Arm pat Nothing body an) cont_a cs
+        . local (typeVars %~ Set.union tvs)
+        . local (names %~ focus ms)
+        . local (classes %~ mappend is)
+        $ check body wanted
+
+  pure
+    (App
+      (w2 (App (w1 bind) expr (an, c1)))
+      (ExprWrapper w3
+        (Fun (PatParam pat')
+          body
+          (an, TyArr cont_a wanted))
+        (an, cont_t))
+      (an, res))
+
 -- This is _very_ annoying, but we need it for nested ascriptions
 check ex@(Ascription e ty an) goal = do
   ty <- expandType =<< resolveKind (becauseExp ex) ty
@@ -412,37 +444,6 @@ infer ex@(ListFromThenTo range_v start next end an) = do
             end (an, c3)) (an, list_t)
        , list_t)
 
-infer ex@(MLet bindv pat expr body an) = do
-  let reason = becauseExp ex
-      bind = VarRef bindv an
-      bind :: Expr Desugared
-  (bind, bind_t) <- infer bind
-
-  ~(Anon action_t, c1, w1) <- quantifier reason (/= Req) bind_t
-  expr <- check expr action_t
-
-  ~(Anon cont_t, res, w2)    <- quantifier reason (/= Req) c1
-  (cont_a, cont_r) <- (,) <$> freshTV <*> freshTV
-  w3 <- subsumes reason (cont_a :-> cont_r) cont_t
-
-  (pat', ms, cs, is) <- checkPattern pat cont_a
-  let tvs = boundTvs pat' ms
-
-  body <- implies (Arm pat Nothing body an) cont_a cs
-        . local (typeVars %~ Set.union tvs)
-        . local (names %~ focus ms)
-        . local (classes %~ mappend is)
-        $ check body cont_r
-
-  pure
-    (App
-      (w2 (App (w1 bind) expr (an, c1)))
-      (ExprWrapper w3
-        (Fun (PatParam pat')
-          body
-          (an, TyArr cont_a cont_r))
-        (an, cont_t))
-      (an, res), res)
 
 infer ex = do
   x <- freshTV

src/Types/Infer/Let.hs

@@ -178,7 +178,7 @@ inferLetTy closeOver strategy vs =
                 exp <- check (exp' exp) tyvar
                 pure (Binding var vp exp True (ann, tyvar), tyvar)
 
-        (solution, wrap, cons) <- solveFixpoint (It'sThis (BecauseInternal "fixed point solving")) cs =<< getSolveInfo
+        (solution, wrap, cons) <- condemn $ solveFixpoint (It'sThis (BecauseInternal "fixed point solving")) cs =<< getSolveInfo
 
         tys <- view tySyms
         if null cons

tests/types/begin04.out

@@ -2,5 +2,5 @@ begin04.ml[21:3 ..22:9]: error (E2001)
    │ 
 21 │   let! y = [2]
    │   ^^^^^^^^^^^^
-  Couldn't match actual type list int
-    with the type expected by the context, identity 'b
+  Couldn't match actual type identity 'b
+    with the type expected by the context, list 'b

tests/types/begin05.out

@@ -3,7 +3,7 @@ begin05.ml[10:3 ..10:3]: error (E2001)
 10 │   2
    │   ^
   Couldn't match actual type int
-    with the type expected by the context, identity 'b
+    with the type expected by the context, identity int
 begin05.ml[8:5 ..11:1]: error (E2018)
   No instance for monad identity arising in the binding
    │