LiquidHaskell Version 0.8.6.0, Git revision 1d8c11324bb718eb3bd5c41643ba4b1cc377abf2 (dirty) [develop@1d8c11324bb718eb3bd5c41643ba4b1cc377abf2 (Thu Jul 11 14:48:47 2019 -0700)] 
Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: resources/custom/liquidhaskell/sandbox/1713907368_17990.hs

**** [Checking: resources/custom/liquidhaskell/sandbox/1713907368_17990.hs] ****

**** DONE:  A-Normalization ****************************************************
 
WARNING: Assume Overwrites Specifications for Lecture_05_ProofsPrograms.fib : /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1713907368_17990.hs:27:13
WARNING: Assume Overwrites Specifications for Lecture_05_ProofsPrograms.sumTo : /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1713907368_17990.hs:92:13

**** DONE:  Extracted Core using GHC *******************************************
 

**** DONE:  Transformed Core ***************************************************
 

**** DONE:  annotate ***********************************************************
 

**** RESULT: UNSAFE ************************************************************


 /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1713907368_17990.hs:10:18-29: Error: Liquid Type Mismatch
  
 10 | intToA x = error "Define me!"
                       ^^^^^^^^^^^^
  
   Inferred type
     VV : {v : [Char] | v ~~ "Define me!"
                        && len v == strLen "Define me!"
                        && len v >= 0
                        && v == "Define me!"}
  
   not a subtype of Required type
     VV : {VV : [Char] | false}
  


 /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1713907368_17990.hs:(80,7)-(83,9): Error: Liquid Type Mismatch
  
 80 |   =   fib x     ? fibUp x
 81 |   =<= fib (x+1) 
 82 |   =<= fib y
 83 |   *** QED
  
   Inferred type
     VV : {v : () | (isAdmit Language.Haskell.Liquid.ProofCombinators.QED => false)
                    && (not (isAdmit Language.Haskell.Liquid.ProofCombinators.QED) => true)}
  
   not a subtype of Required type
     VV : {VV : () | f x <= f y}
  
   In Context
     x : {v : Int | v >= 0}
      
     y : {y : Int | y >= 0
                    && x < y}


 /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1713907368_17990.hs:(85,7)-(88,9): Error: Liquid Type Mismatch
  
 85 |   =   fib x     ? fMonotonic f fUp x (y-1)
 86 |   =<= fib (y-1) ? fibUp (y-1)
 87 |   =<= fib y     
 88 |   *** QED
  
   Inferred type
     VV : {v : () | (isAdmit Language.Haskell.Liquid.ProofCombinators.QED => false)
                    && (not (isAdmit Language.Haskell.Liquid.ProofCombinators.QED) => true)}
  
   not a subtype of Required type
     VV : {VV : () | f x <= f y}
  
   In Context
     x : {v : Int | v >= 0}
      
     y : {y : Int | y >= 0
                    && x < y}


 /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1713907368_17990.hs:86:7-15: Error: Liquid Type Mismatch
  
 86 |   =<= fib (y-1) ? fibUp (y-1)
            ^^^^^^^^^
  
   Inferred type
     VV : {v : Int | v >= 0
                     && v == Lecture_05_ProofsPrograms.fib (y - 1)
                     && v == (if 0 == y - 1 then 0 else (if 1 == y - 1 then 1 else Lecture_05_ProofsPrograms.fib ((y - 1) - 1) + Lecture_05_ProofsPrograms.fib ((y - 1) - 2)))}
  
   not a subtype of Required type
     VV : {VV : Int | ?e <= VV}
  
   In Context
     ?e : Int
      
     x : {v : Int | v >= 0}
      
     y : {y : Int | y >= 0
                    && x < y}