Loaded package environment from /home/liquidhaskell/liquid-server/dist-newstyle/tmp/environment.-156559/.ghc.environment.x86_64-linux-9.12.2 [1 of 1] Compiling Lecture_04_Termination ( resources/custom/liquidhaskell/sandbox/1759855329_16.hs, resources/custom/liquidhaskell/sandbox/1759855329_16.o )  **** LIQUID: UNSAFE ************************************************************ {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":12,"column":25},"end":{"line":12,"column":30}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == i##aQx - (1 : int)}\n .\n is not a subtype of the required type\n VV : {VV##3394 : GHC.Types.Int | VV##3394 >= 0}\n .\n in the context\n ?d : {?d : GHC.Types.Bool | not ?d\n && (?d <=> i##aQx == (0 : int))\n && ?d == (i##aQx == (0 : int))}\n \n ?h : {?h : GHC.Types.Bool | not ?h\n && (?h <=> i##aQx == (1 : int))\n && ?h == (i##aQx == (1 : int))}\n \n i##aQx : GHC.Types.Int\n Constraint id 3"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":12,"column":37},"end":{"line":12,"column":42}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == i##aQx - (2 : int)}\n .\n is not a subtype of the required type\n VV : {VV##3386 : GHC.Types.Int | VV##3386 >= 0}\n .\n in the context\n ?d : {?d : GHC.Types.Bool | not ?d\n && (?d <=> i##aQx == (0 : int))\n && ?d == (i##aQx == (0 : int))}\n \n ?h : {?h : GHC.Types.Bool | not ?h\n && (?h <=> i##aQx == (1 : int))\n && ?h == (i##aQx == (1 : int))}\n \n i##aQx : GHC.Types.Int\n Constraint id 1"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":16,"column":25},"end":{"line":16,"column":31}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == lo##aTg + (1 : int)}\n .\n is not a subtype of the required type\n VV : {VV##3487 : GHC.Types.Int | VV##3487 < lo##aTg}\n .\n in the context\n hi##aTh : GHC.Types.Int\n \n lo##aTg : GHC.Types.Int\n \n ?b : {?b : GHC.Types.Bool | ?b\n && (?b <=> lo##aTg < hi##aTh)\n && ?b == (lo##aTg < hi##aTh)}\n Constraint id 14"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":22,"column":18},"end":{"line":22,"column":23}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == m##aTl - (1 : int)}\n .\n is not a subtype of the required type\n VV : {VV##3545 : GHC.Types.Int | VV##3545 >= 0}\n .\n in the context\n ?d : {?d : GHC.Types.Bool | not ?d\n && (?d <=> m##aTl == (0 : int))\n && ?d == (m##aTl == (0 : int))}\n \n m##aTl : GHC.Types.Int\n Constraint id 17"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":23,"column":21},"end":{"line":23,"column":26}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == m##aTl - (1 : int)}\n .\n is not a subtype of the required type\n VV : {VV##3559 : GHC.Types.Int | VV##3559 >= 0}\n .\n in the context\n ?d : {?d : GHC.Types.Bool | not ?d\n && (?d <=> m##aTl == (0 : int))\n && ?d == (m##aTl == (0 : int))}\n \n m##aTl : GHC.Types.Int\n Constraint id 19"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":23,"column":32},"end":{"line":23,"column":33}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == m##aTl}\n .\n is not a subtype of the required type\n VV : {VV##3563 : GHC.Types.Int | VV##3563 < m##aTl}\n .\n in the context\n ?d : {?d : GHC.Types.Bool | not ?d\n && (?d <=> m##aTl == (0 : int))\n && ?d == (m##aTl == (0 : int))}\n \n m##aTl : GHC.Types.Int\n Constraint id 22"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":29,"column":24},"end":{"line":29,"column":31}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == ?a - b##aTn}\n .\n is not a subtype of the required type\n VV : {VV##3625 : GHC.Types.Int | VV##3625 < ?a}\n .\n in the context\n ?g : {?g : GHC.Prim.Int# | ?g == ?c\n && ?g /= 0}\n \n ?d : {?d : GHC.Types.Int | ?d == ?a\n && ?d == ?b\n && ?d == (?b : int)}\n \n ?f : {?f : GHC.Types.Int | ?f == ?c\n && ?f == b##aTn\n && ?f == (?c : int)}\n \n b##aTn : GHC.Types.Int\n \n ?c : GHC.Prim.Int#\n \n ?a : GHC.Types.Int\n \n ?b : GHC.Prim.Int#\n \n ?k : {?k : GHC.Types.Bool | ?k\n && (?k <=> ?a > b##aTn)\n && ?k == (?a > b##aTn)}\n \n ?i : {?i : GHC.Types.Bool | not ?i\n && (?i <=> ?a == b##aTn)\n && ?i == (?a == b##aTn)}\n \n ?e : {?e : GHC.Prim.Int# | ?e == ?b\n && ?e /= 0}\n Constraint id 28"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":30,"column":24},"end":{"line":30,"column":25}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == ?a}\n .\n is not a subtype of the required type\n VV : {VV##3635 : GHC.Types.Int | VV##3635 < ?a}\n .\n in the context\n ?g : {?g : GHC.Prim.Int# | ?g == ?c\n && ?g /= 0}\n \n ?d : {?d : GHC.Types.Int | ?d == ?a\n && ?d == ?b\n && ?d == (?b : int)}\n \n ?f : {?f : GHC.Types.Int | ?f == ?c\n && ?f == b##aTn\n && ?f == (?c : int)}\n \n b##aTn : GHC.Types.Int\n \n ?c : GHC.Prim.Int#\n \n ?m : {?m : GHC.Types.Bool | ?m\n && (?m <=> ?a < b##aTn)\n && ?m == (?a < b##aTn)}\n \n ?a : GHC.Types.Int\n \n ?b : GHC.Prim.Int#\n \n ?k : {?k : GHC.Types.Bool | not ?k\n && (?k <=> ?a > b##aTn)\n && ?k == (?a > b##aTn)}\n \n ?i : {?i : GHC.Types.Bool | not ?i\n && (?i <=> ?a == b##aTn)\n && ?i == (?a == b##aTn)}\n \n ?e : {?e : GHC.Prim.Int# | ?e == ?b\n && ?e /= 0}\n Constraint id 30"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":34,"column":21},"end":{"line":34,"column":22}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == ?a\n && v >= 0}\n .\n is not a subtype of the required type\n VV : {VV##3685 : GHC.Types.Int | VV##3685 < a##aTr}\n .\n in the context\n ?d : {?d : GHC.Prim.Int# | ?d == ?b\n && ?d /= 0}\n \n a##aTr : {a##aTr : GHC.Types.Int | a##aTr >= 0}\n \n ?c : {?c : GHC.Types.Int | ?c == ?a\n && ?c == ?b\n && ?c == (?b : int)\n && ?c >= 0}\n \n ?a : {?a : GHC.Types.Int | ?a >= 0}\n \n ?b : GHC.Prim.Int#\n Constraint id 40"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":41,"column":21},"end":{"line":41,"column":28}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == a##aTu - b##aTv}\n .\n is not a subtype of the required type\n VV : {VV##3721 : GHC.Types.Int | VV##3721 < a##aTu}\n .\n in the context\n ?b : {?b : GHC.Types.Bool | not ?b\n && (?b <=> a##aTu < b##aTv)\n && ?b == (a##aTu < b##aTv)}\n \n a##aTu : {a##aTu : GHC.Types.Int | a##aTu >= 0}\n \n b##aTv : {b##aTv : GHC.Types.Int | b##aTv >= 0}\n Constraint id 47"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":52,"column":26},"end":{"line":52,"column":28}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : [a] | v == ys##aTE\n && GHC.Types_LHAssumptions.len v >= 0}\n .\n is not a subtype of the required type\n VV : {VV##4474 : [a] | GHC.Types_LHAssumptions.len VV##4474 < GHC.Types_LHAssumptions.len xs##aTz}\n .\n in the context\n y##aTD : a\n \n ?g : {?g : [a] | GHC.Types_LHAssumptions.len ?g == 1 + GHC.Types_LHAssumptions.len xs##aTC\n && head ?g == x##aTB\n && tail ?g == xs##aTC\n && GHC.Types_LHAssumptions.len ?g >= 0}\n \n ?d : {?d : [a] | ?d == ?a\n && ?d == GHC.Types.: y##aTD ys##aTE\n && GHC.Types_LHAssumptions.len ?d == 1 + GHC.Types_LHAssumptions.len ys##aTE\n && head ?d == y##aTD\n && tail ?d == ys##aTE\n && GHC.Types_LHAssumptions.len ?d >= 0}\n \n ?f : {?f : GHC.Types.Bool | not ?f\n && (?f <=> x##aTB < y##aTD)\n && ?f == (x##aTB < y##aTD)}\n \n xs##aTC : {v : [a] | GHC.Types_LHAssumptions.len v >= 0}\n \n ?c : {?c : [a] | ?c == xs##aTz\n && ?c == GHC.Types.: x##aTB xs##aTC\n && GHC.Types_LHAssumptions.len ?c == 1 + GHC.Types_LHAssumptions.len xs##aTC\n && head ?c == x##aTB\n && tail ?c == xs##aTC\n && GHC.Types_LHAssumptions.len ?c >= 0}\n \n xs##aTz : {v : [a] | GHC.Types_LHAssumptions.len v >= 0}\n \n ?h : a\n \n ?a : {?a : [a] | GHC.Types_LHAssumptions.len ?a >= 0}\n \n x##aTB : a\n \n ?b : {?b : [a] | ?b == ?a\n && ?b == GHC.Types.: ?h ?i\n && GHC.Types_LHAssumptions.len ?b == 1 + GHC.Types_LHAssumptions.len ?i\n && head ?b == ?h\n && tail ?b == ?i\n && GHC.Types_LHAssumptions.len ?b >= 0}\n \n ?i : {?i : [a] | GHC.Types_LHAssumptions.len ?i >= 0}\n \n ys##aTE : {ys##aTE : [a] | GHC.Types_LHAssumptions.len ys##aTE >= 0}\n Constraint id 116"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":71,"column":32},"end":{"line":71,"column":43}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : (Lecture_04_Termination.List a) | v == ?g\n && Lecture_04_Termination.llen v == 1 + Lecture_04_Termination.llen xs##aTM\n && Lecture_04_Termination.llen v >= 0}\n .\n is not a subtype of the required type\n VV : {VV##4176 : (Lecture_04_Termination.List a) | Lecture_04_Termination.llen VV##4176 < Lecture_04_Termination.llen xs##aTJ}\n .\n in the context\n ?g : {?g : (Lecture_04_Termination.List a) | Lecture_04_Termination.llen ?g == 1 + Lecture_04_Termination.llen xs##aTM\n && Lecture_04_Termination.llen ?g >= 0}\n \n ?d : {?d : (Lecture_04_Termination.List a) | ?d == ?a\n && ?d == Lecture_04_Termination.Cons y##aTN ys##aTO\n && Lecture_04_Termination.llen ?d == 1 + Lecture_04_Termination.llen ys##aTO\n && Lecture_04_Termination.llen ?d >= 0}\n \n xs##aTJ : {v : (Lecture_04_Termination.List a) | Lecture_04_Termination.llen v >= 0}\n \n ?f : {?f : GHC.Types.Bool | not ?f\n && (?f <=> x##aTL < y##aTN)\n && ?f == (x##aTL < y##aTN)}\n \n ?c : {?c : (Lecture_04_Termination.List a) | ?c == xs##aTJ\n && ?c == Lecture_04_Termination.Cons x##aTL xs##aTM\n && Lecture_04_Termination.llen ?c == 1 + Lecture_04_Termination.llen xs##aTM\n && Lecture_04_Termination.llen ?c >= 0}\n \n ?h : a\n \n ?a : {?a : (Lecture_04_Termination.List a) | Lecture_04_Termination.llen ?a >= 0}\n \n ?b : {?b : (Lecture_04_Termination.List a) | ?b == ?a\n && ?b == Lecture_04_Termination.Cons ?h ?i\n && Lecture_04_Termination.llen ?b == 1 + Lecture_04_Termination.llen ?i\n && Lecture_04_Termination.llen ?b >= 0}\n \n y##aTN : a\n \n ?i : {?i : (Lecture_04_Termination.List a) | Lecture_04_Termination.llen ?i >= 0}\n \n x##aTL : a\n \n ys##aTO : {ys##aTO : (Lecture_04_Termination.List a) | Lecture_04_Termination.llen ys##aTO >= 0}\n \n xs##aTM : {v : (Lecture_04_Termination.List a) | Lecture_04_Termination.llen v >= 0}\n Constraint id 87"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":80,"column":24},"end":{"line":80,"column":25}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n .\n The inferred type\n VV : {v : GHC.Types.Int | v == m##aTQ\n && v >= 0}\n .\n is not a subtype of the required type\n VV : {VV##3763 : GHC.Types.Int | VV##3763 < m##aTQ}\n .\n in the context\n m##aTQ : {m##aTQ : GHC.Types.Int | m##aTQ >= 0}\n Constraint id 53"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":92,"column":1},"end":{"line":92,"column":5}},"severity":"Error","code":null,"message":["Termination Error\nLecture_04_Termination.eval\nNo decreasing parameter"],"hints":[]} {"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1759855329_16.hs","start":{"line":97,"column":1},"end":{"line":97,"column":8}},"severity":"Error","code":null,"message":["Termination Error\nLecture_04_Termination.evalAnd\nNo decreasing parameter"],"hints":[]}