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

[jvanbruegge]

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]

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

[ranjitjhala]

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]

Here is the whole file: Heap.hs

[ranjitjhala]

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]

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

[ranjitjhala]

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]

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]

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

[facundominguez]

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]

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.