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/1657068797_10538.hs  **** [Checking: resources/custom/liquidhaskell/sandbox/1657068797_10538.hs] ****  **** DONE: A-Normalization ****************************************************   **** DONE: annotate ***********************************************************   **** RESULT: ERROR *************************************************************  /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1657068797_10538.hs:(107,15)-(109,2): Error: Illegal type specification for `Tutorial_12_Case_Study_AVL.mkNode` 107 | {-@ mkNode :: a -> l:AVL a -> r:AVL a 108 | -> AVLN a {nodeHeight l r} 109 | @-} Tutorial_12_Case_Study_AVL.mkNode :: a -> (AVL a) -> (AVL a) -> {VV : (AVL a) | realHeight VV == 1 + (if realHeight l > realHeight r then realHeight l else realHeight r)} Sort Error in Refinement: {VV##0 : (Tutorial_12_Case_Study_AVL.AVL a##a3iZ) | Tutorial_12_Case_Study_AVL.realHeight VV##0 == 1 + (if Tutorial_12_Case_Study_AVL.realHeight Tutorial_12_Case_Study_AVL.l > Tutorial_12_Case_Study_AVL.realHeight Tutorial_12_Case_Study_AVL.r then Tutorial_12_Case_Study_AVL.realHeight Tutorial_12_Case_Study_AVL.l else Tutorial_12_Case_Study_AVL.realHeight Tutorial_12_Case_Study_AVL.r)} Cannot unify (Tutorial_12_Case_Study_AVL.AVL @(43)) with func(0 , [(Tutorial_12_Case_Study_AVL.AVL @(44)); (Tutorial_12_Case_Study_AVL.AVL @(44))]) in expression: Tutorial_12_Case_Study_AVL.realHeight Tutorial_12_Case_Study_AVL.l /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1657068797_10538.hs:(143,14)-(147,2): Error: Illegal type specification for `Tutorial_12_Case_Study_AVL.balL0` 143 | {-@ balL0 :: x:a 144 | -> l:{AVLL a x | noHeavy l} 145 | -> r:{AVLR a x | leftBig l r} 146 | -> AVLN a {realHeight l + 1 } 147 | @-} Tutorial_12_Case_Study_AVL.balL0 :: x:a -> l:{VV : (AVL {VV : a | VV < x}) | balFac VV == 0} -> {VV : (AVL {VV : a | x < VV}) | getHeight l - getHeight VV == 2} -> {VV : (AVL a) | realHeight VV == realHeight l + 1} Sort Error in Refinement: {VV##0 : (Tutorial_12_Case_Study_AVL.AVL a##a3qM) | Tutorial_12_Case_Study_AVL.realHeight VV##0 == Tutorial_12_Case_Study_AVL.realHeight Tutorial_12_Case_Study_AVL.l + 1} Cannot unify (Tutorial_12_Case_Study_AVL.AVL @(43)) with func(0 , [(Tutorial_12_Case_Study_AVL.AVL @(44)); (Tutorial_12_Case_Study_AVL.AVL @(44))]) in expression: Tutorial_12_Case_Study_AVL.realHeight Tutorial_12_Case_Study_AVL.l /home/rjhala/research/stack/liquid/liquid-server/resources/custom/liquidhaskell/sandbox/1657068797_10538.hs:(162,14)-(166,2): Error: Illegal type specification for `Tutorial_12_Case_Study_AVL.balR0` 162 | {-@ balR0 :: x:a 163 | -> l: AVLL a x 164 | -> r: {AVLR a x | rightBig l r && noHeavy r} 165 | -> AVLN a {realHeight r + 1} 166 | @-} Tutorial_12_Case_Study_AVL.balR0 :: x:a -> l:(AVL {VV : a | VV < x}) -> {VV : (AVL {VV : a | x < VV}) | getHeight VV - getHeight l == 2 && balFac VV == 0} -> {VV : (AVL a) | realHeight VV == realHeight r + 1} Sort Error in Refinement: {VV##0 : (Tutorial_12_Case_Study_AVL.AVL a##a3e0) | Tutorial_12_Case_Study_AVL.realHeight VV##0 == Tutorial_12_Case_Study_AVL.realHeight Tutorial_12_Case_Study_AVL.r + 1} Cannot unify (Tutorial_12_Case_Study_AVL.AVL @(43)) with func(0 , [(Tutorial_12_Case_Study_AVL.AVL @(44)); (Tutorial_12_Case_Study_AVL.AVL @(44))]) in expression: Tutorial_12_Case_Study_AVL.realHeight Tutorial_12_Case_Study_AVL.r