fix in the proof search. when we start the generation from a template, we must start the refinement from the expression that the typecheker generated

src/runtime/haskell/PGF/TypeCheck.hs

@@ -574,7 +574,7 @@ checkResolvedMetaStore scope e = do
 
 generateForMetas :: Selector s => (Scope -> TType -> TcM s Expr) -> Expr -> TcM s Expr
 generateForMetas prove e = do
-  infExpr emptyScope e
+  (e,_) <- infExpr emptyScope e
   fillinVariables
   refineExpr e
   where