SMTLIB2: Int and Bool incompatible

liquid-crash1.hs

tauren :: /tmp/liquid » tree
.
├── Crash.hs
└── include
    └── Data
        └── Text.spec

2 directories, 2 files

tauren :: /tmp/liquid » cat Crash.hs
{-# Language OverloadedStrings #-}

import qualified Data.Text as T

{-@ x :: {t : T.Text | 0 < tlen t} @-}
x :: T.Text
x =
  let
      isValid xs = T.any (\c -> True) xs
      name''
        | isValid "" = ""
        | otherwise = ""
   in name''
   
tauren :: /tmp/liquid » cat include/Data/Text.spec
module spec Data.Text where

import Data.String

measure tlen :: Data.Text.Text -> { n : Int | 0 <= n }

tauren :: /tmp/liquid » liquid Crash.hs -i include
LiquidHaskell Version 0.8.6.0, Git revision 728b92b12a0d4c14c8c0570d680156fdfc502adb [develop@728b92b12a0d4c14c8c0570d680156fdfc502adb (Tue May 14 22:27:22 2019 -0700)]
Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: Crash.hs

**** [Checking: Crash.hs] ******************************************************

**** DONE:  A-Normalization ****************************************************


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


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

Working  12% [=========........................................................]

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


**** RESULT: ERROR *************************************************************


:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 338 column 86: Sorts Int and Bool are incompatible"
  
tauren :: /tmp/liquid » liquid Crash.hs -i include --prune-unsorted                                                                 
LiquidHaskell Version 0.8.6.0, Git revision 728b92b12a0d4c14c8c0570d680156fdfc502adb [develop@728b92b12a0d4c14c8c0570d680156fdfc502adb (Tue May 14 22:27:22 2019 -0700)]
Copyright 2013-19 Regents of the University of California. All Rights Reserved.

Targets: Crash.hs

**** [Checking: Crash.hs] ******************************************************

**** DONE:  A-Normalization ****************************************************


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


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

Working  12% [=========........................................................]

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


**** RESULT: ERROR *************************************************************


:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 338 column 86: Sorts Int and Bool are incompatible"