LH/LF is not aware that Strings are Lists

[AlecsFerra]

The following code crashes LF

{-# LANGUAGE GADTs #-}

{-@ LIQUID "--ple"           @-}
{-@ LIQUID "--reflection"    @-}
{-@ LIQUID "--save"          @-}

module Printf where

import Language.Haskell.Liquid.Prelude
import Language.Haskell.Liquid.ProofCombinators


{-@ reflect countPlaceholders @-}
countPlaceholders :: String -> Int
countPlaceholders (x : xs) | x == '%'  = 1 + countPlaceholders xs
                           | otherwise = 0 + countPlaceholders xs
countPlaceholders []                   = 0

{-@ lemma :: { countPlaceholders "% %!" = 2 } @-}
lemma :: Proof
lemma = trivial

example = liquidAssert (countPlaceholders "% %!" == 2) True

With error

<no location info>: error:
    Fixpoint.Types.dummyLoc:1:1-1:1: Error
  elaborate askSMT failed on:
      is$GHC.Types.[] ("% %!" : Str)
  with error
      Cannot unify [@(593)] with Str in expression: is$GHC.Types.[] ("% %!" : Str) 
  in environment
      is$GHC.Types.[] := func(1 , [[@(0)]; bool])

Even worst if we comment out lemma, it fails verification silently of the assertion inside example even if PLE should be able to prove it by simple unfolds of countPlaceholders

The issue is caused by the fact that to LF Strings and list of characters are different things even if in Haskell String is just a type alias for [Char].

[AlecsFerra]

I see multiple solutions:

• Doing the conversion (String -> [Char]) before sending everything to LF
• The LF type system should allow the unification Str ~ [Chr], this doesn't lock us out from using theories that are only available for strings even tough at least for z3 it looks like that sequences can do everything strings can do
• Just drop the Str type in LF and treat it as an alias for [Chr]