8

I have a server in Haskell that responds to Json inputs. The problem is that there are cases where the server will crash because of a partial function, but Liquid Haskell says it is safe.

Here's a minimal working example:

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DeriveGeneric #-}

module Main where

import qualified Web.Scotty as Scot
import GHC.Generics (Generic)
import qualified Data.Aeson as Json
import Data.Text.Internal.Lazy (Text)

main :: IO ()
main =
  Scot.scotty 3000 $
    Scot.get "/:queryJson" $ do
      rawRequest <- Scot.param "queryJson"
      case Json.decode rawRequest of
        Nothing -> Scot.text "Could not decode input."
        Just input -> Scot.text $ makeOutput (dim1 input)

{-@ type Dim = { x : Int | x >= 0 && x <= 1 } @-}

{-@ makeOutput :: Dim -> Text @-}
makeOutput :: Int -> Text
makeOutput dim =
  case dim of
    0 -> "a"
    1 -> "b"
    _ -> error "Liquid haskell should stop this happening."

{-@ dim1 :: Input -> Dim @-}
data Input = Input
  { dim1 :: Int
  } deriving (Generic)

instance Json.FromJSON Input

Liquid Haskell says that this is safe, but I can crash it by visiting http://localhost:3000/{"dim1":2}.

What I would like is for Liquid Haskell to tell me that the annotation for the 'dim1' function is not valid, because it can't be sure that the input will be 0 or 1.

Edit:

I have found that if I manually make an access function for dim1 in Input, like:

{-@ dim1get :: Input -> Dim @-}
dim1get :: Input -> Int
dim1get (Input x) = x

and use that instead of the 'dim1' function, then I get the required warning from Liquid Haskell that the code is unsafe.

8n8
  • 1,233
  • 1
  • 8
  • 21
  • Have you made a bug report on github? The devs are amazingly responsive. – Thomas M. DuBuisson Mar 30 '18 at 14:52
  • No not yet. But if you think it is one then that gives me more confidence that it is one, and not just a silly mistake on my part. – 8n8 Mar 30 '18 at 18:32
  • 2
    Yes, I think this is a bug. I've (albeit long ago) ran into trivial bugs in the totality checker so I don't have an illusion that the tool is perfect or heavily tested - the team is just too small and there really isn't a "Liquid Haskell community" to help. – Thomas M. DuBuisson Mar 30 '18 at 18:43

0 Answers0