LiquidHaskell Version 0.8.6.0, Git revision 82c7ca2fd5e224b0709e32da9e70c84c692c655e (dirty) [develop@82c7ca2fd5e224b0709e32da9e70c84c692c655e (Mon Oct 7 17:24:07 2019 +0200)] Copyright 2013-19 Regents of the University of California. All Rights Reserved. Targets: resources/custom/liquidhaskell/sandbox/1741868594_1547.hs  **** [Checking: resources/custom/liquidhaskell/sandbox/1741868594_1547.hs] *****  **** DONE: A-Normalization ****************************************************  WARNING: Assume Overwrites Specifications for Tutorial_09_Case_Study_Lazy_Queues.size : /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:64:10  **** DONE: Extracted Core using GHC *******************************************   **** DONE: Transformed Core ***************************************************  WARNING: Found false in /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:15:5 WARNING: Found false in /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:15:15  **** DONE: annotate ***********************************************************   **** RESULT: UNSAFE ************************************************************  /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:71:1-17: Error: Liquid Type Mismatch 71 | badList = SL 1 [] -- rejected ^^^^^^^^^^^^^^^^^ Inferred type VV : {v : [a] | Tutorial_09_Case_Study_Lazy_Queues.realSize v == 0 && len v == 0 && len v >= 0 && v == ?a} not a subtype of Required type VV : {VV : [a] | Tutorial_09_Case_Study_Lazy_Queues.realSize VV == 1} In Context ?a : {?a : [a] | Tutorial_09_Case_Study_Lazy_Queues.realSize ?a == 0 && len ?a == 0 && len ?a >= 0} /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:92:13-23: Error: Liquid Type Mismatch 92 | badHd = hd' (tl okList) -- rejected ^^^^^^^^^^^ Inferred type VV : {v : (Tutorial_09_Case_Study_Lazy_Queues.SList [GHC.Types.Char]) | Tutorial_09_Case_Study_Lazy_Queues.size v == Tutorial_09_Case_Study_Lazy_Queues.size Tutorial_09_Case_Study_Lazy_Queues.okList - 1 && Tutorial_09_Case_Study_Lazy_Queues.size v >= 0 && v == ?a} not a subtype of Required type VV : {VV : (Tutorial_09_Case_Study_Lazy_Queues.SList [GHC.Types.Char]) | Tutorial_09_Case_Study_Lazy_Queues.size VV > 0} In Context Tutorial_09_Case_Study_Lazy_Queues.okList : {Tutorial_09_Case_Study_Lazy_Queues.okList : (Tutorial_09_Case_Study_Lazy_Queues.SList [GHC.Types.Char]) | Tutorial_09_Case_Study_Lazy_Queues.size Tutorial_09_Case_Study_Lazy_Queues.okList == 1 && Tutorial_09_Case_Study_Lazy_Queues.size Tutorial_09_Case_Study_Lazy_Queues.okList >= 0} ?a : {?a : (Tutorial_09_Case_Study_Lazy_Queues.SList [GHC.Types.Char]) | Tutorial_09_Case_Study_Lazy_Queues.size ?a == Tutorial_09_Case_Study_Lazy_Queues.size Tutorial_09_Case_Study_Lazy_Queues.okList - 1 && Tutorial_09_Case_Study_Lazy_Queues.size ?a >= 0} /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:105:14-19: Error: Liquid Type Mismatch 105 | badQ = Q nil okList -- rejected, |front| < |back| ^^^^^^ Inferred type VV : {v : (Tutorial_09_Case_Study_Lazy_Queues.SList [GHC.Types.Char]) | Tutorial_09_Case_Study_Lazy_Queues.size v == 1 && Tutorial_09_Case_Study_Lazy_Queues.size v >= 0 && v == Tutorial_09_Case_Study_Lazy_Queues.okList} not a subtype of Required type VV : {VV : (Tutorial_09_Case_Study_Lazy_Queues.SList [GHC.Types.Char]) | Tutorial_09_Case_Study_Lazy_Queues.size VV <= Tutorial_09_Case_Study_Lazy_Queues.size ?a} In Context Tutorial_09_Case_Study_Lazy_Queues.okList : {Tutorial_09_Case_Study_Lazy_Queues.okList : (Tutorial_09_Case_Study_Lazy_Queues.SList [GHC.Types.Char]) | Tutorial_09_Case_Study_Lazy_Queues.size Tutorial_09_Case_Study_Lazy_Queues.okList == 1 && Tutorial_09_Case_Study_Lazy_Queues.size Tutorial_09_Case_Study_Lazy_Queues.okList >= 0} ?a : {?a : (Tutorial_09_Case_Study_Lazy_Queues.SList [GHC.Types.Char]) | Tutorial_09_Case_Study_Lazy_Queues.size ?a == 0 && Tutorial_09_Case_Study_Lazy_Queues.size ?a >= 0} /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:127:1-28: Error: Liquid Type Mismatch 127 | badRemove = remove example0Q -- reject ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Inferred type VV : {v : (Tutorial_09_Case_Study_Lazy_Queues.Queue a) | Tutorial_09_Case_Study_Lazy_Queues.qsize v == 0 && v == ?a} not a subtype of Required type VV : {VV : (Tutorial_09_Case_Study_Lazy_Queues.Queue a) | Tutorial_09_Case_Study_Lazy_Queues.qsize VV > 0} In Context ?a : {?a : (Tutorial_09_Case_Study_Lazy_Queues.Queue a) | Tutorial_09_Case_Study_Lazy_Queues.qsize ?a == 0} /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:136:1-33: Error: Liquid Type Mismatch 136 | okReplicate = replicate 3 "Yeah!" -- accept ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Inferred type VV : (Tutorial_09_Case_Study_Lazy_Queues.Queue [GHC.Types.Char]) not a subtype of Required type VV : {VV : (Tutorial_09_Case_Study_Lazy_Queues.Queue [GHC.Types.Char]) | Tutorial_09_Case_Study_Lazy_Queues.qsize VV == 3} /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:139:1-32: Error: Liquid Type Mismatch 139 | badReplicate = replicate 1 "No!" -- reject ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Inferred type VV : (Tutorial_09_Case_Study_Lazy_Queues.Queue [GHC.Types.Char]) not a subtype of Required type VV : {VV : (Tutorial_09_Case_Study_Lazy_Queues.Queue [GHC.Types.Char]) | Tutorial_09_Case_Study_Lazy_Queues.qsize VV == 3} /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:145:24-42: Error: Liquid Type Mismatch 145 | | otherwise = Q (rot f b nil) nil ^^^^^^^^^^^^^^^^^^^ Inferred type VV : {v : (Tutorial_09_Case_Study_Lazy_Queues.Queue a) | Tutorial_09_Case_Study_Lazy_Queues.back v == ?a && Tutorial_09_Case_Study_Lazy_Queues.front v == ?c && Tutorial_09_Case_Study_Lazy_Queues.qsize v == Tutorial_09_Case_Study_Lazy_Queues.size ?c + Tutorial_09_Case_Study_Lazy_Queues.size ?a} not a subtype of Required type VV : {VV : (Tutorial_09_Case_Study_Lazy_Queues.Queue a) | Tutorial_09_Case_Study_Lazy_Queues.qsize VV == Tutorial_09_Case_Study_Lazy_Queues.size f + Tutorial_09_Case_Study_Lazy_Queues.size b} In Context ?c : {?c : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size ?c == Tutorial_09_Case_Study_Lazy_Queues.size ?b && Tutorial_09_Case_Study_Lazy_Queues.size ?c >= 0} b : {b : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size b <= Tutorial_09_Case_Study_Lazy_Queues.size f + 1 && Tutorial_09_Case_Study_Lazy_Queues.size b >= 0} ?b : {?b : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size ?b == 0 && Tutorial_09_Case_Study_Lazy_Queues.size ?b >= 0} f : {f : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size f >= 0} ?a : {?a : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size ?a == 0 && Tutorial_09_Case_Study_Lazy_Queues.size ?a >= 0} /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:145:33: Error: Liquid Type Mismatch 145 | | otherwise = Q (rot f b nil) nil ^ Inferred type VV : {v : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size v <= Tutorial_09_Case_Study_Lazy_Queues.size f + 1 && Tutorial_09_Case_Study_Lazy_Queues.size v >= 0 && v == b} not a subtype of Required type VV : {VV : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size VV == 1 - Tutorial_09_Case_Study_Lazy_Queues.size f} In Context b : {b : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size b <= Tutorial_09_Case_Study_Lazy_Queues.size f + 1 && Tutorial_09_Case_Study_Lazy_Queues.size b >= 0} f : {f : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size f >= 0} /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:152:19-33: Error: Liquid Type Mismatch 152 | | size f == 0 = hd b `cons` acc ^^^^^^^^^^^^^^^ Inferred type VV : {v : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size v == Tutorial_09_Case_Study_Lazy_Queues.size acc + 1 && Tutorial_09_Case_Study_Lazy_Queues.size v >= 0} not a subtype of Required type VV : {VV : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size VV == Tutorial_09_Case_Study_Lazy_Queues.size acc} In Context acc : {acc : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size acc >= 0} /home/liquidhaskell/liquid-server/resources/custom/liquidhaskell/sandbox/1741868594_1547.hs:153:44: Error: Liquid Type Mismatch 153 | | otherwise = hd f `cons` rot (tl f) (tl b) (hd b `cons` acc) ^ Inferred type VV : {v : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size v == 1 - Tutorial_09_Case_Study_Lazy_Queues.size f && Tutorial_09_Case_Study_Lazy_Queues.size v >= 0 && v == b} not a subtype of Required type VV : {VV : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size VV > 0} In Context b : {b : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size b == 1 - Tutorial_09_Case_Study_Lazy_Queues.size f && Tutorial_09_Case_Study_Lazy_Queues.size b >= 0} f : {f : (Tutorial_09_Case_Study_Lazy_Queues.SList a) | Tutorial_09_Case_Study_Lazy_Queues.size f >= 0}