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/1679922141_713.hs  **** [Checking: resources/custom/liquidhaskell/sandbox/1679922141_713.hs] ******  **** DONE: A-Normalization ****************************************************   **** DONE: Extracted Core using GHC *******************************************   **** DONE: Transformed Core ***************************************************   **** DONE: annotate ***********************************************************   **** RESULT: UNSAFE ************************************************************  /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1679922141_713.hs:108:30-36: Error: Liquid Type Mismatch 108 | | otherwise = initialize f (i + 1) n (set i (f i) a) ^^^^^^^ Inferred type VV : {v : Int | v == i + 1} not a subtype of Required type VV : {VV : Int | VV >= 0 && VV < i} In Context i : {i : Int | i >= 0} /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1679922141_713.hs:144:12: Error: Liquid Type Mismatch 144 | c -> ucs n (i + 1) (set i (c + 32) s) ^ Inferred type VV : {v : Int | v == n} not a subtype of Required type VV : {VV : Int | VV < n && VV >= 0} In Context n : Int /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1679922141_713.hs:154:1-31: Error: Liquid Type Mismatch 154 | upperCaseString n s = ucs n 0 s ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Inferred type VV : Int not a subtype of Required type VV : {VV : Int | ?a == n - 1 => VV == 0} In Context n : {n : Int | n > 0} ?a : {?a : Int | 0 <= ?a && ?a < n} /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1679922141_713.hs:154:31: Error: Liquid Type Mismatch 154 | upperCaseString n s = ucs n 0 s ^ Inferred type VV : Int not a subtype of Required type VV : {VV : Int | 0 <= VV && VV < n} In Context n : {n : Int | n > 0}