Fix laziness bookkeeping in unification

Need to note we can't add a laziness coercion under 'unifyInvertible',
which is where we unify things under metavariables which are known to
stand for constructor forms. Fixes #360

src/Core/Unify.idr

@@ -675,13 +675,13 @@ mutual
   unifyHoleApp swap mode loc env mname mref margs margs' (NTCon nfc n t a args')
       = do defs <- get Ctxt
            mty <- lookupTyExact n (gamma defs)
-           unifyInvertible swap mode loc env mname mref margs margs' mty (NTCon nfc n t a) args'
+           unifyInvertible swap (lower mode) loc env mname mref margs margs' mty (NTCon nfc n t a) args'
   unifyHoleApp swap mode loc env mname mref margs margs' (NDCon nfc n t a args')
       = do defs <- get Ctxt
            mty <- lookupTyExact n (gamma defs)
-           unifyInvertible swap mode loc env mname mref margs margs' mty (NTCon nfc n t a) args'
+           unifyInvertible swap (lower mode) loc env mname mref margs margs' mty (NTCon nfc n t a) args'
   unifyHoleApp swap mode loc env mname mref margs margs' (NApp nfc (NLocal r idx p) args')
-      = unifyInvertible swap mode loc env mname mref margs margs' Nothing
+      = unifyInvertible swap (lower mode) loc env mname mref margs margs' Nothing
                         (NApp nfc (NLocal r idx p)) args'
   unifyHoleApp swap mode loc env mname mref margs margs' tm@(NApp nfc (NMeta n i margs2) args2')
       = do defs <- get Ctxt
@@ -689,7 +689,7 @@ mutual
                 | Nothing => throw (UndefinedName nfc mname)
            let inv = isPatName n || invertible mdef
            if inv
-              then unifyInvertible swap mode loc env mname mref margs margs' Nothing
+              then unifyInvertible swap (lower mode) loc env mname mref margs margs' Nothing
                                    (NApp nfc (NMeta n i margs2)) args2'
               else postponeS True swap loc mode "Postponing hole application" env
                              (NApp loc (NMeta mname mref margs) margs') tm

tests/Main.idr

@@ -81,7 +81,7 @@ idrisTests
        -- Miscellaneous regressions
        "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
-       "reg015", "reg016", "reg017", "reg018",
+       "reg015", "reg016", "reg017", "reg018", "reg019",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006",

tests/idris2/reg019/expected

@@ -0,0 +1,16 @@
+1/1: Building lazybug (lazybug.idr)
+lazybug.idr:5:22--5:34:While processing right hand side of main at lazybug.idr:5:1--7:1:
+Can't solve constraint between:
+	Bool
+and
+	Lazy Bool
+lazybug.idr:8:23--8:42:While processing right hand side of main2 at lazybug.idr:8:1--10:1:
+Can't solve constraint between:
+	Bool
+and
+	Lazy Bool
+lazybug.idr:14:22--15:1:While processing right hand side of main4 at lazybug.idr:14:1--15:1:
+Can't solve constraint between:
+	Bool
+and
+	Lazy Bool

tests/idris2/reg019/lazybug.idr

@@ -0,0 +1,14 @@
+bools : List Bool
+bools = [True, False]
+
+main : IO ()
+main = printLn $ or (map id bools)
+
+main2 : IO ()
+main2 = printLn $ or (map (\x => x) bools)
+
+main3 : IO ()
+main3 = printLn $ or (map (\x => Delay x) bools)
+
+main4 : IO ()
+main4 = printLn $ or bools

tests/idris2/reg019/run

@@ -0,0 +1,3 @@
+$1 lazybug.idr --check
+
+rm -rf build