https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/38

liquidhaskell_tutorial_chapter_3_log_20160504

src$ date
Wed May  4 10:36:38 JST 2016
src$ liquid 03-basic.lhs 
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.


**** DONE:  Parsed All Specifications ******************************************
 

**** DONE:  Loaded Targets *****************************************************
 

**** DONE:  Extracted Core using GHC *******************************************
 
Working  17% [============.....................................................]
Done solving.

**** DONE:  solve **************************************************************
 

**** START: pandoc *************************************************************
 

**** DONE:  pandoc *************************************************************
 

**** START: pandoc *************************************************************
 

**** DONE:  pandoc *************************************************************
 
WARNING: Found false in 03-basic.lhs:192:5-7

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

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


 03-basic.lhs:70:1-4: Error: Liquid Type Mismatch
 
 70 | one' = 1 :: Int
      ^^^^
 
   Inferred type
     VV : {VV : Int | VV == (1 : int)}
  
   not a subtype of Required type
     VV : {VV : Int | VV == 0}
  
   In Context


 03-basic.lhs:214:21-36: Error: Liquid Type Mismatch
 
 214 |            then die "horrible death"
                           ^^^^^^^^^^^^^^^^
 
   Inferred type
     VV : {VV : [Char] | VV == ?a
                         && len VV >= 0}
  
   not a subtype of Required type
     VV : {VV : [Char] | false}
  
   In Context
     ?a := {?a : [Char] | ?a ~~ ?b
                          && len ?a == strLen ?b
                          && len ?a >= 0}

     ?b := {?b : Addr# | ?b ~~ "horrible death"
                         && strLen ?b == 14}


 03-basic.lhs:393:23-47: Error: Liquid Type Mismatch
 
 393 | lAssert False _ = die "yikes, assertion fails!"
                             ^^^^^^^^^^^^^^^^^^^^^^^^^
 
   Inferred type
     VV : {VV : [Char] | VV == ?b
                         && len VV >= 0}
  
   not a subtype of Required type
     VV : {VV : [Char] | false}
  
   In Context
     ?a := {?a : Addr# | ?a ~~ "yikes, assertion fails!"
                         && strLen ?a == 23}

     ?b := {?b : [Char] | ?b ~~ ?a
                          && len ?b == strLen ?a
                          && len ?b >= 0}
src$ cat avg.hs
{-@ LIQUID "--short-names" @-}

{-@ type NonZero = {v:Int | v /= 0} @-}

{-@ die :: {v:String | false} -> a @-}
die :: String -> a
die msg = error msg

{-@ divide :: Int -> NonZero -> Int @-}
divide :: Int -> Int -> Int
divide _ 0 = die "divide by zero"
divide n d = n `div` d

avg :: [Int] -> Int
avg xs = divide total n
  where
    total = sum xs
    n = length xs
src$ liquid avg.hs 
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.


**** DONE:  Parsed All Specifications ******************************************
 

**** DONE:  Loaded Targets *****************************************************
 

**** DONE:  Extracted Core using GHC *******************************************
 
Working  50% [=================================................................]
Done solving.

**** DONE:  solve **************************************************************
 
WARNING: Found false in avg.hs:7:5-7

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

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


 avg.hs:15:10-23: Error: Liquid Type Mismatch
 
 15 | avg xs = divide total n
               ^^^^^^^^^^^^^^
 
   Inferred type
     VV : {VV : Int | VV == n}
  
   not a subtype of Required type
     VV : {VV : Int | VV /= 0}
  
   In Context
     xs := {v : [Int] | len v >= 0}

     n := {n : Int | n >= 0
                     && n == len xs}
src$ liquid --version
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.
src$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.10.3
src$