search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.18k stars 136 forks source link

GADT without refinement throws "specified type does not refine Haskell type" error #2287

Open jvanbruegge opened 4 months ago

jvanbruegge commented 4 months ago

The following code

data Nat = Zero | Succ Nat
  deriving stock Show

data Tree (k :: Nat) a where
  MkTree :: a -> DecList Tree k a -> Tree k a

data DecList (t :: Nat -> Type -> Type) (k :: Nat) (a :: Type) where
  DNil :: DecList t Zero a
  DCons :: t k a -> DecList t k a -> DecList t (Succ k) a

data Binary
  = B0 Binary
  | B1 Binary
  | BEnd
  deriving stock Show

data Forest k b a where
  FEnd :: Forest k BEnd a
  F0 :: Forest (Succ k) b a -> Forest k (B0 b) a
  F1 :: Tree k a -> Forest (Succ k) b a -> Forest k (B1 b) a

throws an error for the Forest type:

src/Heap.hs:58:3: error:
    Specified type does not refine Haskell type for `Heap.$WF1` (Plugged Init types new - TC disallowed)
The Liquid type
.
    forall k a b b##X0 .
    (Heap.Tree k a) -> (Heap.Forest 'Heap.Succ b a) -> (Heap.Forest k ('Heap.B1 b) a)
.
is inconsistent with the Haskell type
.
    forall (k :: Heap.Nat) a (b :: Heap.Binary).
Heap.Tree k a
%1 -> Heap.Forest ('Heap.Succ k) b a
%1 -> Heap.Forest k ('Heap.B1 b) a
.
defined at src/Heap.hs:58:3-60
.
Specifically, the Liquid component
.
    'Heap.Succ
.
is inconsistent with the Haskell component
.
    ('Heap.Succ k)
.

HINT: Use the hole '_' instead of the mismatched component (in the Liquid specification)
   |
58 |   F1 :: Tree k a -> Forest (Succ k) b a -> Forest k (B1 b) a
   |

However, the definition is accepted if converted to existential style:

data Forest k b a =
  b ~ BEnd => FEnd
  | forall b'. b ~ B0 b' => F0 (Forest (Succ k) b' a)
  | forall b'. b ~ B1 b' => F1 (Tree k a) (Forest (Succ k) b' a)

but sadly this fails when trying to prove anything using reflect:

type family BInc (binary :: Binary) :: Binary where
  BInc BEnd = B1 BEnd
  BInc (B0 rest) = B1 rest
  BInc (B1 rest) = B0 (BInc rest)

{-@ reflect pot @-}
pot :: Forest k b a -> Int
pot FEnd = 0
pot (F0 rest) = pot rest
pot (F1 _ rest) = 1 + pot rest

{-@ reflect insertTree @-}
insertTree :: Ord a => Tree k a -> Forest k b a -> Forest k (BInc b) a
insertTree t FEnd = F1 t FEnd
insertTree t (F0 f) = F1 t f
insertTree t (F1 t' f) = F0 (insertTree (mergeTree t t') f)

{-@ insertTreeAmortized :: t:_ -> f:_ -> { insertTreeT t f + pot (insertTree t f) - pot f <= 2 } @-}
insertTreeAmortized :: Ord a => Tree k a -> Forest k b a -> Proof
insertTreeAmortized t f@FEnd =
  insertTreeT t f + pot (insertTree t f) - pot f
    === 1 + pot (insertTree t f) - 0
    === 1 + pot (F1 t FEnd) -- fails
    === undefined

with the error

src/Heap.hs:110:9: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v == GHC.Num.+ (GHC.Types.I# 1) (Heap.pot (Heap.F1 t##ac2u Heap.FEnd))
                                && v == GHC.Types.I# 1 + Heap.pot (Heap.F1 t##ac2u Heap.FEnd)}
    .
    is not a subtype of the required type
      VV : {VV##16932 : GHC.Types.Int | VV##16932 == GHC.Num.- (GHC.Num.+ (Heap.insertTreeT t##ac2u Heap.FEnd) (Heap.pot (coerce (Heap.Forest k##acoD (Heap.BInc b##acoE) a##acoC) ~ (Heap.Forest k##acoD (Heap.B1 Heap.BEnd) a##acoC) in Heap.insertTree t##ac2u Heap.FEnd))) (Heap.pot Heap.FEnd)}
    .
    in the context
      t##ac2u : (Heap.Tree a b)

      f##ac2v : (Heap.Forest a b c)
    Constraint id 273
    |
110 |     === 1 + pot (F1 t FEnd) -- fails
    |
jvanbruegge commented 4 months ago

I also tried add a refinement type signature and replace pretty much everything with underscores but that did not help either

ranjitjhala commented 4 months ago

I think LH simply does not “know” about these newer GHC features. That said, can you post your mergeTree code? Ideally all the Nat stuff should just be in refinements so I wonder if we can make a simpler version work…

jvanbruegge commented 4 months ago

Here is the whole file: Heap.hs

ranjitjhala commented 4 months ago

Thanks! The below seems to work fine:

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
{-# LANGUAGE GADTs #-}

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

module Heap where

import Language.Haskell.Liquid.Equational

-------------------------------------------------------------------------------

data Binary
  = B0 Binary
  | B1 Binary
  | BEnd

data DecList t a where
  DNil  :: DecList t a
  DCons :: t a -> DecList t a -> DecList t a

data Tree a where
  MkTree :: a -> DecList Tree a -> Tree a

data Forest a where
    FEnd :: Forest a
    F0   :: Forest a -> Forest a
    F1   :: Tree a -> Forest a -> Forest a

{-@ measure pot @-}
{-@ pot :: Forest a -> Nat @-}
pot :: Forest a -> Int
pot FEnd        = 0
pot (F0 rest)   = pot rest
pot (F1 _ rest) = 1 + pot rest

{-@ reflect mergeTree @-}
mergeTree :: Ord a => Tree a -> Tree a -> Tree a
mergeTree l@(MkTree lr lc) r@(MkTree rr rc)
  | lr <= rr = MkTree lr (DCons r lc)
  | otherwise = MkTree rr (DCons l rc)

{-@ reflect insertTree @-}
insertTree :: Ord a => Tree a -> Forest a -> Forest a
insertTree t FEnd = F1 t FEnd
insertTree t (F0 f) = F1 t f
insertTree t (F1 t' f) = F0 (insertTree (mergeTree t t') f)

{-@ reflect insertTreeT @-}
insertTreeT :: Ord a => Tree a -> Forest a -> Int
insertTreeT _ FEnd = 1
insertTreeT _ (F0 _) = 1
insertTreeT t (F1 t' f) = 1 + insertTreeT (mergeTree t t') f

{-@ insertTreeAmortized :: t:_ -> f:_ -> { insertTreeT t f + pot (insertTree t f) - pot f <= 2 } @-}
insertTreeAmortized :: Ord a => Tree a -> Forest a -> Proof
insertTreeAmortized t FEnd         = ()
insertTreeAmortized t (F0 rest)    = ()
insertTreeAmortized t (F1 t' rest) = insertTreeAmortized (mergeTree t t') rest
jvanbruegge commented 4 months ago

Yeah, not using GADTs works, but I was hoping to use fancy types to ensure correctness. Is DataKinds just not supported by LH?

ranjitjhala commented 4 months ago

I don't think so, sadly. Maybe @facundominguez and @nikivazou know more? [ I think there was some very limited support but perhaps its rather brittle? ]

ranjitjhala commented 4 months ago

I think "in theory" it shouldn't be hard, because LH doesn't really need to know much about them -- just follow GHC -- but I think "in practice" we just haven't updated the connection ... ?

ranjitjhala commented 4 months ago

Hmm this is a very interesting use of the DataKinds -- thanks for pointing it out!

facundominguez commented 4 months ago

LH doesn't really need to know much about them

This would be my expectation, but I haven't worked with this part of the code base yet.

nikivazou commented 4 months ago

Well, from the error message, it seems that the refined type for the "worker" data constructor Heap.$WF1 is not well produced.

GHC generates two types of data constructors, the worker and the the wrapper. In Liquid Haskell we generate the type of the worker based on the user provided type. I suspect that these newer GHC features generate more fancy worker types. So, even though LH does not need to know much about these features, we need to at least, update the generation of the worker type.