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