LiquidHaskell Copyright 2009-14 Regents of the University of California. All Rights Reserved.

Warning: Couldn't do create temp directory: ./.liquid: createDirectory: already exists (File exists)
parseSpec: zipW.hs
paths = ["/home/travis/build/spinda/liquidhaskell/tests/pos","/home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/"]
getSpecs: [("NotReal","/home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/NotReal.spec"),("Language.Haskell.Liquid.Prelude","/home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/Language/Haskell/Liquid/Prelude.hs"),("Prelude","/home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/Prelude.spec")]
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/NotReal.spec
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/Language/Haskell/Liquid/Prelude.hs
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/Prelude.spec
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/GHC/Num.spec
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/GHC/Base.spec
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/GHC/Int.spec
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/GHC/List.spec
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/GHC/Real.spec
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/GHC/Word.spec
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/Data/Maybe.spec
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/GHC/Prim.spec
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/GHC/Classes.spec
parseSpec: /home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/GHC/Types.spec
Module Imports: ["Data.Maybe","GHC.Base","GHC.Classes","GHC.Exts","GHC.Int","GHC.List","GHC.Num","GHC.Prim","GHC.Real","GHC.Types","GHC.Word","Language.Haskell.Liquid.Prelude","Prelude"]
Reading Qualifiers From: ["/home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/GHC/Base.hquals","/home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/Prelude.hquals"]

**** DONE:  Extracted Core using GHC *******************************************
 
**** Config **************************************************
Config {files = ["zipW.hs"], idirs = ["/home/travis/build/spinda/liquidhaskell/tests/pos","/home/travis/build/spinda/liquidhaskell/.cabal-sandbox/share/x86_64-linux-ghc-7.8.4/liquidhaskell-0.3.1.0/include/"], diffcheck = False, real = False, fullcheck = False, binders = [], noCheckUnknown = False, notermination = False, nowarnings = False, trustinternals = False, nocaseexpand = False, strata = False, notruetypes = False, totality = False, noPrune = False, maxParams = 2, smtsolver = Just cvc4, shortNames = False, shortErrors = False, ghcOptions = [], cFiles = []}
*************** Imports *********************
Data.Maybe, GHC.Base, GHC.Classes, GHC.Exts, GHC.Int, GHC.List, GHC.Num, GHC.Prim, GHC.Real, GHC.Types, GHC.Word, Language.Haskell.Liquid.Prelude, Prelude
*************** Includes ********************
*************** Imported Variables **********
[GHC.CString.unpackCString#, GHC.Types.:, GHC.Types.[],
 Language.Haskell.Liquid.Prelude.liquidError]
*************** Defined Variables ***********
[T.zipW, a, b, c, f, ds_d14x, ds_d14y, lq_anf__d14B, lq_anf__d14C,
 ds_d14z, ds_d14A, lq_anf__d14D, a, as, lq_anf__d14E, lq_anf__d14F,
 b, bs, lq_anf__d14G, lq_anf__d14H, T.foo, a, b, c]
*************** Specification ***************
******* Target Variables ********************
[]
******* Type Signatures *********************
[GHC.Classes.&& : x:GHC.Types.Bool -> y:GHC.Types.Bool -> {v : GHC.Types.Bool | Prop v <=> Prop x && Prop y}
 GHC.List.takeWhile : lq_tmp_db24:(lq_tmp_db25:a -> GHC.Types.Bool) -> xs:[a] -> {v : [a] | len v <= len xs}
 GHC.List.length : xs:[a] -> {v : GHC.Types.Int | v == len xs}
 GHC.Real.fromIntegral : (GHC.Real.Integral a, GHC.Num.Num b) =>
                         x:a -> {VV : b | VV == x}
 GHC.List.!! : xs:[a] -> lq_tmp_db36:{v : GHC.Types.Int | 0 <= v && v < len xs} -> a
 Language.Haskell.Liquid.Prelude.safeZipWith : lq_tmp_db8:(lq_tmp_db9:a -> lq_tmp_db10:b -> c) -> xs:[a] -> ys:{v : [b] | len v == len xs} -> {v : [c] | len v == len xs}
 GHC.Types.True : {v : GHC.Types.Bool | Prop v}
 GHC.List.take : n:GHC.Types.Int -> xs:[a] -> {v : [a] | (n >= 0 => len v == (if len xs < n then len xs else n)) && (not (n >= 0) => len v == 0)}
 GHC.List.last : xs:{v : [a] | len v > 0} -> a
 GHC.Real./ : (GHC.Real.Fractional a) =>
              x:a -> y:{VV : a | VV /= 0} -> {VV : a | VV == x / y}
 GHC.List.replicate : n:{v : GHC.Types.Int | v >= 0} -> x:a -> {v : [{VV : a | VV == x}] | len v == n}
 GHC.Classes.>= : (GHC.Classes.Ord a) =>
                  x:a -> y:a -> {v : GHC.Types.Bool | Prop v <=> x >= y}
 GHC.List.cycle : lq_tmp_db23:{v : [a] | len v > 0} -> [a]
 GHC.Types.EQ : {v : GHC.Types.Ordering | v == cmp v}
 GHC.Types.False : {v : GHC.Types.Bool | not (Prop v)}
 GHC.List.repeat : lq_tmp_db22:a -> [a]
 GHC.Base.map : lq_tmp_db5:(lq_tmp_db6:a -> b) -> xs:[a] -> {v : [b] | len v == len xs}
 GHC.Num.negate : (GHC.Num.Num a) => x:a -> {VV : a | VV == (-x)}
 GHC.Types.LT : {v : GHC.Types.Ordering | v == cmp v}
 GHC.List.zipWith : lq_tmp_db37:(lq_tmp_db38:a -> lq_tmp_db39:b -> c) -> xs:[a] -> ys:[b] -> {v : [c] | len v <= len xs && len v <= len ys}
 GHC.Classes.|| : x:GHC.Types.Bool -> y:GHC.Types.Bool -> {v : GHC.Types.Bool | Prop v <=> Prop x || Prop y}
 GHC.List.break : lq_tmp_db32:(lq_tmp_db33:a -> GHC.Types.Bool) -> xs:[a] -> ([a], [a])
 GHC.Types.isTrue# : n:GHC.Prim.Int# -> {v : GHC.Types.Bool | n == 1 <=> Prop v}
 GHC.Types.GT : {v : GHC.Types.Ordering | v == cmp v}
 GHC.List.null : xs:[a] -> {v : GHC.Types.Bool | Prop v <=> len xs == 0}
 GHC.Base.$ : lq_tmp_db7:(lq_tmp_db8:a -> b) -> lq_tmp_db9:a -> b
 GHC.Classes.not : x:GHC.Types.Bool -> {v : GHC.Types.Bool | Prop v <=> not (Prop x)}
 GHC.Classes.<= : (GHC.Classes.Ord a) =>
                  x:a -> y:a -> {v : GHC.Types.Bool | Prop v <=> x <= y}
 GHC.Real.mod : (GHC.Real.Integral a) =>
                x:a -> y:{VV : a | VV /= 0} -> {VV : a | VV == x mod y && (0 <= x && 0 < y => 0 <= VV && VV < y)}
 GHC.List.scanr : lq_tmp_db12:(lq_tmp_db13:a -> lq_tmp_db14:b -> b) -> lq_tmp_db15:b -> xs:[a] -> {v : [b] | len v == 1 + len xs}
 GHC.Classes.< : (GHC.Classes.Ord a) =>
                 x:a -> y:a -> {v : GHC.Types.Bool | Prop v <=> x < y}
 GHC.Real.divMod : (GHC.Real.Integral a) =>
                   lq_tmp_db7:a -> lq_tmp_db8:{VV : a | VV /= 0} -> (a, a)
 GHC.List.scanl1 : lq_tmp_db6:(lq_tmp_db7:a -> lq_tmp_db8:a -> a) -> xs:{v : [a] | len v > 0} -> {v : [a] | len v == len xs}
 GHC.Classes./= : (GHC.Classes.Eq a) =>
                  x:a -> y:a -> {v : GHC.Types.Bool | Prop v <=> x /= y}
 GHC.Real.div : (GHC.Real.Integral a) =>
                x:a -> y:{VV : a | VV /= 0} -> {VV : a | VV == x / y && (x >= 0 && y >= 0 => VV >= 0) && (x >= 0 && y >= 1 => VV <= x)}
 GHC.List.scanl : lq_tmp_db2:(lq_tmp_db3:b -> lq_tmp_db4:a -> b) -> lq_tmp_db5:b -> xs:[a] -> {v : [b] | len v == 1 + len xs}
 GHC.List.dropWhile : lq_tmp_db26:(lq_tmp_db27:a -> GHC.Types.Bool) -> xs:[a] -> {v : [a] | len v <= len xs}
 GHC.Types.D# : x:GHC.Prim.Double# -> {v : GHC.Types.Double | v == x}
 GHC.Real.recip : (GHC.Real.Fractional a) => lq_tmp_db1:a -> a
 GHC.List.reverse : xs:[a] -> {v : [a] | len v == len xs}
 GHC.Classes.== : (GHC.Classes.Eq a) =>
                  x:a -> y:a -> {v : GHC.Types.Bool | Prop v <=> x == y}
 GHC.List.drop : n:GHC.Types.Int -> xs:[a] -> {v : [a] | (n >= 0 => len v == (if len xs < n then 0 else len xs - n)) && (not (n >= 0) => len v == len xs)}
 T.zipW : lq_tmp_db0:(lq_tmp_db1:a -> lq_tmp_db2:b -> c) -> xs:[a] -> ys:{v : [b] | len v == len xs} -> {v : [c] | len v == len xs}
 GHC.List.filter : lq_tmp_db0:(lq_tmp_db1:a -> GHC.Types.Bool) -> xs:[a] -> {v : [a] | len v <= len xs}
 GHC.Classes.min : (GHC.Classes.Ord a) =>
                   x:a -> y:a -> {VV : a | VV == (if x < y then x else y)}
 GHC.List.tail : xs:{v : [a] | len v > 0} -> {v : [a] | len v == len xs - 1}
 Language.Haskell.Liquid.Prelude.==> : p:GHC.Types.Bool -> q:GHC.Types.Bool -> {v : GHC.Types.Bool | Prop v <=> (Prop p => Prop q)}
 GHC.Num.fromInteger : (GHC.Num.Num a) =>
                       x:GHC.Integer.Type.Integer -> {VV : a | VV == x}
 GHC.List.iterate : lq_tmp_db19:(lq_tmp_db20:a -> a) -> lq_tmp_db21:a -> [a]
 GHC.Real.toInteger : (GHC.Real.Integral a) =>
                      x:a -> {v : GHC.Integer.Type.Integer | v == x}
 GHC.List.zip : xs:[a] -> ys:[b] -> {v : [(a, b)] | len v <= len xs && len v <= len ys && (len xs == len ys => len v == len xs)}
 GHC.Classes.max : (GHC.Classes.Ord a) =>
                   x:a -> y:a -> {VV : a | VV == (if x > y then x else y)}
 GHC.Real.rem : (GHC.Real.Integral a) =>
                lq_tmp_db5:a -> lq_tmp_db6:{VV : a | VV /= 0} -> a
 GHC.List.splitAt : n:GHC.Types.Int -> x:[a] -> ({v : [a] | (n >= 0 => (len x < n => len v == len x) && (not (len x < n) => len v == n)) && (not (n >= 0) => len v == 0)}, [a])
 GHC.List.init : xs:{v : [a] | len v > 0} -> {v : [a] | len v == len xs - 1}
 T.foo : lq_tmp_db3:(lq_tmp_db4:a -> lq_tmp_db5:b -> c) -> xs:[a] -> ys:{v : [b] | len v == len xs} -> {v : [c] | len v == len xs}
 GHC.Classes.compare : (GHC.Classes.Ord a) =>
                       x:a -> y:a -> {v : GHC.Types.Ordering | (v == GHC.Types.EQ#6U <=> x == y) && (v == GHC.Types.LT#6S <=> x < y) && (v == GHC.Types.GT#6W <=> x > y)}
 GHC.Real.quotRem : (GHC.Real.Integral a) =>
                    x:a -> y:{VV : a | VV /= 0} -> ({VV : a | VV == x / y && (x >= 0 && y >= 0 => VV >= 0) && (x >= 0 && y >= 1 => VV <= x)}, {VV : a | VV >= 0 && VV < y})
 GHC.List.span : lq_tmp_db30:(lq_tmp_db31:a -> GHC.Types.Bool) -> xs:[a] -> ({v : [a] | len v <= len xs}, {v : [a] | len v <= len xs})
 GHC.Real.fromRational : (GHC.Real.Fractional a) =>
                         lq_tmp_db2:(GHC.Real.Ratio GHC.Integer.Type.Integer) -> a
 GHC.List.head : xs:{v : [a] | len v > 0} -> a
 GHC.Base.id : x:a -> {VV : a | VV == x}
 GHC.Classes.> : (GHC.Classes.Ord a) =>
                 x:a -> y:a -> {v : GHC.Types.Bool | Prop v <=> x > y}
 GHC.Base.++ : xs:[a] -> ys:[a] -> {v : [a] | len v == len xs + len ys}
 GHC.Real.quot : (GHC.Real.Integral a) =>
                 lq_tmp_db3:a -> lq_tmp_db4:{VV : a | VV /= 0} -> a
 GHC.List.scanr1 : lq_tmp_db16:(lq_tmp_db17:a -> lq_tmp_db18:a -> a) -> xs:{v : [a] | len v > 0} -> {v : [a] | len v == len xs}
 GHC.List.foldr1 : lq_tmp_db9:(lq_tmp_db10:a -> lq_tmp_db11:a -> a) -> xs:{v : [a] | len v > 0} -> a
 GHC.List.errorEmptyList : lq_tmp_db40:{v : [GHC.Types.Char] | false} -> a]
******* Assumed Type Signatures *************
[GHC.Num.* : (GHC.Num.Num a) =>
             x:a -> y:a -> {VV : a | (x == 0 || y == 0 => VV == 0) && (x > 0 && y > 0 => VV >= x && VV >= y) && (x > 1 && y > 1 => VV > x && VV > y)}
 Language.Haskell.Liquid.Prelude.plus : x:GHC.Types.Int -> y:GHC.Types.Int -> {v : GHC.Types.Int | v == x + y}
 Language.Haskell.Liquid.Prelude.minus : x:GHC.Types.Int -> y:GHC.Types.Int -> {v : GHC.Types.Int | v == x - y}
 Language.Haskell.Liquid.Prelude.times : x:GHC.Types.Int -> y:GHC.Types.Int -> GHC.Types.Int
 Language.Haskell.Liquid.Prelude.eq : x:GHC.Types.Int -> y:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x == y}
 Language.Haskell.Liquid.Prelude.neq : x:GHC.Types.Int -> y:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x /= y}
 Language.Haskell.Liquid.Prelude.leq : x:GHC.Types.Int -> y:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x <= y}
 Language.Haskell.Liquid.Prelude.geq : x:GHC.Types.Int -> y:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x >= y}
 Language.Haskell.Liquid.Prelude.lt : x:GHC.Types.Int -> y:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x < y}
 Language.Haskell.Liquid.Prelude.gt : x:GHC.Types.Int -> y:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x > y}
 Language.Haskell.Liquid.Prelude.liquidAssertB : x:{v : GHC.Types.Bool | Prop v} -> {v : GHC.Types.Bool | Prop v}
 Language.Haskell.Liquid.Prelude.liquidAssert : lq_tmp_db0:{v : GHC.Types.Bool | Prop v} -> lq_tmp_db1:a -> a
 Language.Haskell.Liquid.Prelude.liquidAssume : b:GHC.Types.Bool -> lq_tmp_db2:a -> {VV : a | Prop b}
 Language.Haskell.Liquid.Prelude.liquidAssumeB : lq_tmp_db4:(lq_tmp_db5:{VV : a | true} -> {v : GHC.Types.Bool | Prop v <=> true}) -> lq_tmp_db6:a -> {VV : a | true}
 Language.Haskell.Liquid.Prelude.liquidError : lq_tmp_db7:{VV : [GHC.Types.Char] | 0 == 1} -> a
 Language.Haskell.Liquid.Prelude.crash : x:{v : GHC.Types.Bool | Prop v} -> a
 Language.Haskell.Liquid.Prelude.isEven : x:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x mod 2 == 0}
 Language.Haskell.Liquid.Prelude.isOdd : x:GHC.Types.Int -> {v : GHC.Types.Bool | Prop v <=> x mod 2 == 1}
 GHC.Base.. : {xcmp :: a, wcmp :: {VV : b | true} |- {VV : c | true} <: {VV : c | true}} =>
              lq_tmp_db6:(ycmp:b -> {VV : c | true}) -> lq_tmp_db7:(zcmp:a -> {VV : b | true}) -> xcmp:a -> {VV : c | true}
 GHC.Integer.Type.smallInteger : x:GHC.Prim.Int# -> {v : GHC.Integer.Type.Integer | v == (x : int)}
 GHC.Num.+ : (GHC.Num.Num a) => x:a -> y:a -> {VV : a | VV == x + y}
 GHC.Num.- : (GHC.Num.Num a) => x:a -> y:a -> {VV : a | VV == x - y}
 GHC.Types.I# : x:GHC.Prim.Int# -> {v : GHC.Types.Int | v == (x : int)}
 GHC.Prim.+# : x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v : GHC.Prim.Int# | v == x + y}
 GHC.Prim.-# : x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v : GHC.Prim.Int# | v == x - y}
 GHC.Prim.==# : x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v : GHC.Prim.Int# | v == 1 <=> x == y}
 GHC.Prim.>=# : x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v : GHC.Prim.Int# | v == 1 <=> x >= y}
 GHC.Prim.<=# : x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v : GHC.Prim.Int# | v == 1 <=> x <= y}
 GHC.Prim.<# : x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v : GHC.Prim.Int# | v == 1 <=> x < y}
 GHC.Prim.># : x:GHC.Prim.Int# -> y:GHC.Prim.Int# -> {v : GHC.Prim.Int# | v == 1 <=> x > y}]
******* DataCon Specifications (Measure) ****
[GHC.Tuple.(,,,,,) : xx1:a -> xx2:{VV : b | true} -> xx3:{VV : c | true} -> xx4:{VV : d | true} -> xx5:{VV : e | true} -> xx6:{VV : f | true} -> {VV : (a, b, c, d, e, f) | x_Tuple66 VV == xx6 && x_Tuple65 VV == xx5 && x_Tuple64 VV == xx4 && x_Tuple63 VV == xx3 && x_Tuple62 VV == xx2 && x_Tuple61 VV == xx1}
 GHC.Tuple.(,,,,,,) : xx1:a -> xx2:{VV : b | true} -> xx3:{VV : c | true} -> xx4:{VV : d | true} -> xx5:{VV : e | true} -> xx6:{VV : f | true} -> xx7:{VV : g | true} -> {VV : (a, b, c, d, e, f, g) | x_Tuple77 VV == xx7 && x_Tuple76 VV == xx6 && x_Tuple75 VV == xx5 && x_Tuple74 VV == xx4 && x_Tuple73 VV == xx3 && x_Tuple72 VV == xx2 && x_Tuple71 VV == xx1}
 Data.Maybe.Just : x:a -> {VV : (Data.Maybe.Maybe a) | fromJust VV == x && (isJust VV <=> true)}
 GHC.Types.EQ : {VV : GHC.Types.Ordering | cmp VV == GHC.Types.EQ#6U}
 GHC.Tuple.(,,,) : xx1:a -> xx2:{VV : b | true} -> xx3:{VV : c | true} -> xx4:{VV : d | true} -> {VV : (a, b, c, d) | x_Tuple44 VV == xx4 && x_Tuple43 VV == xx3 && x_Tuple42 VV == xx2 && x_Tuple41 VV == xx1}
 GHC.Types.LT : {VV : GHC.Types.Ordering | cmp VV == GHC.Types.LT#6S}
 GHC.Types.GT : {VV : GHC.Types.Ordering | cmp VV == GHC.Types.GT#6W}
 GHC.Tuple.(,,,,) : xx1:a -> xx2:{VV : b | true} -> xx3:{VV : c | true} -> xx4:{VV : d | true} -> xx5:{VV : e | true} -> {VV : (a, b, c, d, e) | x_Tuple55 VV == xx5 && x_Tuple54 VV == xx4 && x_Tuple53 VV == xx3 && x_Tuple52 VV == xx2 && x_Tuple51 VV == xx1}
 GHC.Real.D:Integral : (GHC.Real.Real a, GHC.Enum.Enum a) =>
                       GHC.Real.quot_GHC.Real.D:Integral#r6o:(lq_tmp_db3:a -> lq_tmp_db4:{VV : a | VV /= 0} -> a) -> GHC.Real.rem_GHC.Real.D:Integral#r6o:(lq_tmp_db5:a -> lq_tmp_db6:{VV : a | VV /= 0} -> a) -> GHC.Real.mod_GHC.Real.D:Integral#r6o:(x:a -> y:{VV : a | VV /= 0} -> {VV : a | VV == x mod y && (0 <= x && 0 < y => 0 <= VV && VV < y)}) -> GHC.Real.div_GHC.Real.D:Integral#r6o:(x:a -> y:{VV : a | VV /= 0} -> {VV : a | VV == x / y && (x >= 0 && y >= 0 => VV >= 0) && (x >= 0 && y >= 1 => VV <= x)}) -> GHC.Real.quotRem_GHC.Real.D:Integral#r6o:(x:a -> y:{VV : a | VV /= 0} -> ({VV : a | VV == x / y && (x >= 0 && y >= 0 => VV >= 0) && (x >= 0 && y >= 1 => VV <= x)}, {VV : a | VV >= 0 && VV < y})) -> GHC.Real.divMod_GHC.Real.D:Integral#r6o:(lq_tmp_db7:a -> lq_tmp_db8:{VV : a | VV /= 0} -> (a, a)) -> GHC.Real.toInteger_GHC.Real.D:Integral#r6o:(x:a -> {v : GHC.Integer.Type.Integer | v == x}) -> (GHC.Real.Integral a)
 GHC.Tuple.(,) : a:a -> b:{VV : b | true} -> {VV : (a, b) | snd VV == b && fst VV == a && x_Tuple22 VV == b && x_Tuple21 VV == a}
 GHC.Types.: : x:a -> xs:[{VV : a | true}] -> {VV : [a] | (null VV <=> false) && len VV == 1 + len xs && xsListSelector VV == xs && xListSelector VV == x}
 GHC.Tuple.(,,) : xx1:a -> xx2:{VV : b | true} -> xx3:{VV : c | true} -> {VV : (a, b, c) | x_Tuple33 VV == xx3 && x_Tuple32 VV == xx2 && x_Tuple31 VV == xx1}
 GHC.Types.[] : {VV : [a] | (null VV <=> true) && len VV == 0}
 Data.Maybe.Nothing : {VV : (Data.Maybe.Maybe a) | isJust VV <=> false}
 GHC.Real.D:Fractional : (GHC.Num.Num a) =>
                         (GHC.Real./)_GHC.Real.D:Fractional#rkT:(x:a -> y:{VV : a | VV /= 0} -> {VV : a | VV == x / y}) -> GHC.Real.recip_GHC.Real.D:Fractional#rkT:(lq_tmp_db1:a -> a) -> GHC.Real.fromRational_GHC.Real.D:Fractional#rkT:(lq_tmp_db2:(GHC.Real.Ratio GHC.Integer.Type.Integer) -> a) -> (GHC.Real.Fractional a)]
******* Measure Specifications **************
[x_Tuple61 : (a, b, c, d, e, f) -> a
 x_Tuple43 : (a, b, c, d) -> c
 x_Tuple51 : (a, b, c, d, e) -> a
 x_Tuple73 : (a, b, c, d, e, f, g) -> c
 x_Tuple54 : (a, b, c, d, e) -> d
 x_Tuple76 : (a, b, c, d, e, f, g) -> f
 x_Tuple32 : (a, b, c) -> b
 cmp : lq_tmp_db0:GHC.Types.Ordering -> GHC.Types.Ordering
 fst : lq_tmp_db3:(a, b) -> a
 snd : lq_tmp_db4:(a, b) -> b
 x_Tuple42 : (a, b, c, d) -> b
 x_Tuple74 : (a, b, c, d, e, f, g) -> d
 len : lq_tmp_db1:[a] -> GHC.Types.Int
 x_Tuple66 : (a, b, c, d, e, f) -> f
 x_Tuple44 : (a, b, c, d) -> d
 x_Tuple22 : (a, b) -> b
 xListSelector : [a] -> a
 x_Tuple72 : (a, b, c, d, e, f, g) -> b
 isJust : lq_tmp_db0:(Data.Maybe.Maybe a) -> Prop
 x_Tuple75 : (a, b, c, d, e, f, g) -> e
 Prop : lq_tmp_db0:GHC.Types.Bool -> Prop
 x_Tuple31 : (a, b, c) -> a
 x_Tuple52 : (a, b, c, d, e) -> b
 null : lq_tmp_db2:[a] -> Prop
 x_Tuple62 : (a, b, c, d, e, f) -> b
 fromJust : lq_tmp_db1:(Data.Maybe.Maybe a) -> a
 x_Tuple53 : (a, b, c, d, e) -> c
 x_Tuple71 : (a, b, c, d, e, f, g) -> a
 addrLen : lq_tmp_db0:GHC.Prim.Addr# -> GHC.Types.Int
 x_Tuple65 : (a, b, c, d, e, f) -> e
 x_Tuple21 : (a, b) -> a
 xsListSelector : [a] -> [a]
 x_Tuple55 : (a, b, c, d, e) -> e
 x_Tuple33 : (a, b, c) -> c
 x_Tuple77 : (a, b, c, d, e, f, g) -> g
 x_Tuple63 : (a, b, c, d, e, f) -> c
 x_Tuple41 : (a, b, c, d) -> a
 x_Tuple64 : (a, b, c, d, e, f) -> d]
*************** Core Bindings ***************
[T.zipW [Occ=LoopBreaker]
   :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
 [LclIdX, Str=DmdType]
 T.zipW =
   \ (@ a)
     (@ b)
     (@ c)
     (f :: a -> b -> c)
     (ds_d14x :: [a])
     (ds_d14y :: [b]) ->
     case ds_d14x of lq_anf__d14B {
       [] ->
         case ds_d14y of lq_anf__d14C {
           [] -> GHC.Types.[] @ c;
           : _ [Occ=Dead] _ [Occ=Dead] ->
             let {
               lq_anf__d14D :: [GHC.Types.Char]
               [LclId, Str=DmdType]
               lq_anf__d14D = GHC.CString.unpackCString# "zipWith1"# } in
             Language.Haskell.Liquid.Prelude.liquidError @ [c] lq_anf__d14D
         };
       : a as ->
         case ds_d14y of lq_anf__d14E {
           [] ->
             let {
               lq_anf__d14F :: [GHC.Types.Char]
               [LclId, Str=DmdType]
               lq_anf__d14F = GHC.CString.unpackCString# "zipWith1"# } in
             Language.Haskell.Liquid.Prelude.liquidError @ [c] lq_anf__d14F;
           : b bs ->
             let {
               lq_anf__d14G :: c
               [LclId, Str=DmdType]
               lq_anf__d14G = f a b } in
             let {
               lq_anf__d14H :: [c]
               [LclId, Str=DmdType]
               lq_anf__d14H = T.zipW @ a @ b @ c f as bs } in
             GHC.Types.: @ c lq_anf__d14G lq_anf__d14H
         }
     };,
 T.foo :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
 [LclIdX, Str=DmdType]
 T.foo = \ (@ a) (@ b) (@ c) -> T.zipW @ a @ b @ c]
*************** Original CoreBinds ***************************
[T.zipW [Occ=LoopBreaker]
   :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
 [LclIdX, Str=DmdType]
 T.zipW =
   \ (@ a)
     (@ b)
     (@ c)
     (f :: a -> b -> c)
     (ds_d14x :: [a])
     (ds_d14y :: [b]) ->
     case ds_d14x of lq_anf__d14B {
       [] ->
         case ds_d14y of lq_anf__d14C {
           [] -> GHC.Types.[] @ c;
           : _ [Occ=Dead] _ [Occ=Dead] ->
             let {
               lq_anf__d14D :: [GHC.Types.Char]
               [LclId, Str=DmdType]
               lq_anf__d14D = GHC.CString.unpackCString# "zipWith1"# } in
             Language.Haskell.Liquid.Prelude.liquidError @ [c] lq_anf__d14D
         };
       : a as ->
         case ds_d14y of lq_anf__d14E {
           [] ->
             let {
               lq_anf__d14F :: [GHC.Types.Char]
               [LclId, Str=DmdType]
               lq_anf__d14F = GHC.CString.unpackCString# "zipWith1"# } in
             Language.Haskell.Liquid.Prelude.liquidError @ [c] lq_anf__d14F;
           : b bs ->
             let {
               lq_anf__d14G :: c
               [LclId, Str=DmdType]
               lq_anf__d14G = f a b } in
             let {
               lq_anf__d14H :: [c]
               [LclId, Str=DmdType]
               lq_anf__d14H = T.zipW @ a @ b @ c f as bs } in
             GHC.Types.: @ c lq_anf__d14G lq_anf__d14H
         }
     };,
 T.foo :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
 [LclIdX, Str=DmdType]
 T.foo = \ (@ a) (@ b) (@ c) -> T.zipW @ a @ b @ c]

**** DONE:  transformRecExpr ***************************************************
 
*************** Transform Rec Expr CoreBinds *****************
[T.zipW [Occ=LoopBreaker]
   :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
 [LclIdX, Str=DmdType]
 T.zipW =
   \ (@ a)
     (@ b)
     (@ c)
     (f :: a -> b -> c)
     (ds_d14x :: [a])
     (ds_d14y :: [b]) ->
     case ds_d14x of lq_anf__d14B {
       [] ->
         case ds_d14y of lq_anf__d14C {
           [] -> GHC.Types.[] @ c;
           : _ [Occ=Dead] _ [Occ=Dead] ->
             let {
               lq_anf__d14D :: [GHC.Types.Char]
               [LclId, Str=DmdType]
               lq_anf__d14D = GHC.CString.unpackCString# "zipWith1"# } in
             Language.Haskell.Liquid.Prelude.liquidError @ [c] lq_anf__d14D
         };
       : a as ->
         case ds_d14y of lq_anf__d14E {
           [] ->
             let {
               lq_anf__d14F :: [GHC.Types.Char]
               [LclId, Str=DmdType]
               lq_anf__d14F = GHC.CString.unpackCString# "zipWith1"# } in
             Language.Haskell.Liquid.Prelude.liquidError @ [c] lq_anf__d14F;
           : b bs ->
             let {
               lq_anf__d14G :: c
               [LclId, Str=DmdType]
               lq_anf__d14G = f a b } in
             let {
               lq_anf__d14H :: [c]
               [LclId, Str=DmdType]
               lq_anf__d14H = T.zipW @ a @ b @ c f as bs } in
             GHC.Types.: @ c lq_anf__d14G lq_anf__d14H
         }
     };,
 T.foo :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
 [LclIdX, Str=DmdType]
 T.foo = \ (@ a) (@ b) (@ c) -> T.zipW @ a @ b @ c]
*************** Slicing Out Unchanged CoreBinds *****************

**** DONE:  generateConstraints ************************************************
 
liquid: 
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************
Cannot find fixpoint binary [fixpoint.native]
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************