Loaded package environment from /home/liquidhaskell/liquid-server/dist-newstyle/tmp/environment.-3144868/.ghc.environment.x86_64-linux-9.12.2
[1 of 1] Compiling Tutorial_02_Logic ( resources/custom/liquidhaskell/sandbox/1748034493_821.hs, resources/custom/liquidhaskell/sandbox/1748034493_821.o )

**** LIQUID: UNSAFE ************************************************************
{"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1748034493_821.hs","start":{"line":48,"column":1},"end":{"line":48,"column":13}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n    .\n    The inferred type\n      VV : {v : GHC.Types.Bool | not v\n                                 && v == False}\n    .\n    is not a subtype of the required type\n      VV : {VV##3422 : GHC.Types.Bool | VV##3422}\n    .\n    Constraint id 87"],"hints":[]}
{"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1748034493_821.hs","start":{"line":59,"column":1},"end":{"line":59,"column":26}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n    .\n    The inferred type\n      VV : {v : GHC.Types.Bool | (v <=> (?a => a##aQw))\n                                 && v == ==> ?a a##aQw}\n    .\n    is not a subtype of the required type\n      VV : {VV##3646 : GHC.Types.Bool | VV##3646}\n    .\n    in the context\n      ?a : {?a : GHC.Types.Bool | (?a <=> a##aQw\n                                          || b##aQx)\n                                  && ?a == || a##aQw b##aQx}\n       \n      a##aQw : GHC.Types.Bool\n       \n      b##aQx : GHC.Types.Bool\n    Constraint id 97"],"hints":[]}
{"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1748034493_821.hs","start":{"line":68,"column":1},"end":{"line":68,"column":52}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n    .\n    The inferred type\n      VV : {v : GHC.Types.Bool | (v <=> (?b <=> ?e))\n                                 && v == <=> ?b ?e}\n    .\n    is not a subtype of the required type\n      VV : {VV##3450 : GHC.Types.Bool | VV##3450}\n    .\n    in the context\n      ?d : {?d : GHC.Types.Bool | (?d <=> not b##aQF)\n                                  && ?d == not b##aQF}\n       \n      ?c : {?c : GHC.Types.Bool | (?c <=> not a##aQE)\n                                  && ?c == not a##aQE}\n       \n      ?a : {?a : GHC.Types.Bool | (?a <=> a##aQE\n                                          && b##aQF)\n                                  && ?a == && a##aQE b##aQF}\n       \n      ?b : {?b : GHC.Types.Bool | (?b <=> not ?a)\n                                  && ?b == not ?a}\n       \n      b##aQF : GHC.Types.Bool\n       \n      ?e : {?e : GHC.Types.Bool | (?e <=> ?c\n                                          && ?d)\n                                  && ?e == && ?c ?d}\n       \n      a##aQE : GHC.Types.Bool\n    Constraint id 89"],"hints":[]}
{"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1748034493_821.hs","start":{"line":72,"column":1},"end":{"line":72,"column":18}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n    .\n    The inferred type\n      VV : {v : GHC.Types.Bool | (v <=> ?e == ?g)\n                                 && v == == ?e ?g}\n    .\n    is not a subtype of the required type\n      VV : {VV##3358 : GHC.Types.Bool | VV##3358}\n    .\n    in the context\n      ?g : {?g : GHC.Num.Integer.Integer | ?g == IS 3\n                                           && ?g == (3 : int)}\n       \n      ?d : {?d : GHC.Num.Integer.Integer | ?d == IS 1\n                                           && ?d == (1 : int)}\n       \n      ?b : {?b : GHC.Num.Integer.Integer | ?b == IS 1\n                                           && ?b == (1 : int)}\n       \n      ?e : {?e : GHC.Num.Integer.Integer | ?e == + ?b ?d\n                                           && ?e == ?b + ?d}\n    Constraint id 79"],"hints":[]}
{"version":"1.1","ghcVersion":"ghc-9.12.2","span":{"file":"resources/custom/liquidhaskell/sandbox/1748034493_821.hs","start":{"line":89,"column":1},"end":{"line":89,"column":32}},"severity":"Error","code":null,"message":["Liquid Type Mismatch\n    .\n    The inferred type\n      VV : {v : GHC.Types.Bool | (v <=> (True => ?b))\n                                 && v == ==> True ?b}\n    .\n    is not a subtype of the required type\n      VV : {VV##2510 : GHC.Types.Bool | VV##2510}\n    .\n    in the context\n      y##aTB : GHC.Types.Int\n       \n      x##aTA : GHC.Types.Int\n       \n      ?a : {?a : GHC.Types.Int | ?a == + x##aTA y##aTB\n                                 && ?a == x##aTA + y##aTB}\n       \n      ?b : {?b : GHC.Types.Bool | (?b <=> x##aTA <= ?a)\n                                  && ?b == <= x##aTA ?a}\n    Constraint id 1"],"hints":[]}