@@ -1019,12 +1019,12 @@ mutual
10191019 case mix of
10201020 Nothing =>
10211021 do log " compile.casetree.intermediate" 25 " match: No clauses"
1022- pure (Unmatched " No clauses" )
1022+ pure (Unmatched " No clauses in \{show fn} " )
10231023 Just m =>
10241024 do log " compile.casetree.intermediate" 25 $ " match: new case tree " ++ show m
10251025 Core . pure m
10261026 match {todo = []} fc fn phase [] err
1027- = maybe (pure (Unmatched " No patterns" ))
1027+ = maybe (pure (Unmatched " No patterns in \{show fn} " ))
10281028 pure err
10291029 match {todo = []} fc fn phase ((MkPatClause pvars [] pid (Erased _ Impossible )) :: _ ) err
10301030 = pure Impossible
@@ -1066,7 +1066,7 @@ mutual
10661066 List (PatClause (a :: todo) vars) ->
10671067 Maybe (CaseTree vars) ->
10681068 Core (CaseTree vars)
1069- conRule fc fn phase [] err = maybe (pure (Unmatched " No constructor clauses" )) pure err
1069+ conRule fc fn phase [] err = maybe (pure (Unmatched " No constructor clauses in \{show fn} " )) pure err
10701070 -- ASSUMPTION, not expressed in the type, that the patterns all have
10711071 -- the same variable (pprf) for the first argument. If not, the result
10721072 -- will be a broken case tree... so we should find a way to express this
@@ -1214,7 +1214,7 @@ patCompile : {auto c : Ref Ctxt Defs} ->
12141214 Maybe (CaseTree Scope.empty) ->
12151215 Core (args ** CaseTree args)
12161216patCompile fc fn phase ty [] def
1217- = maybe (pure (Scope . empty ** Unmatched " No definition " ))
1217+ = maybe (pure (Scope . empty ** Unmatched " \{show fn} not defined " ))
12181218 (\ e => pure (Scope . empty ** e))
12191219 def
12201220patCompile fc fn phase ty (p :: ps) def
@@ -1372,7 +1372,7 @@ getPMDef : {auto c : Ref Ctxt Defs} ->
13721372getPMDef fc phase fn ty []
13731373 = do log " compile.casetree.getpmdef" 20 " getPMDef: No clauses!"
13741374 defs <- get Ctxt
1375- pure (cast ! (getArgs 0 ! (nf defs Env . empty ty)) ** (Unmatched " No clauses" , []))
1375+ pure (cast ! (getArgs 0 ! (nf defs Env . empty ty)) ** (Unmatched " No clauses in \{show fn} " , []))
13761376 where
13771377 getArgs : Int -> ClosedNF -> Core (List Name)
13781378 getArgs i (NBind fc x (Pi _ _ _ _ ) sc)
0 commit comments