Refined GADTs with deriving confuse the type checker

The following GADT type checks just fine:

{-@ LIQUID "--exact-data-cons" @-}
{-@ LIQUID "--prune-unsorted"  @-}
{-# LANGUAGE NoOverloadedLists #-}
{-# LANGUAGE NoOverloadedStrings, DataKinds, KindSignatures, TypeApplications, GADTs #-}
module Base where

import Prelude
import Data.List.NonEmpty
import Data.Text hiding (append)

data BindingType = State | Data

data ABinding :: BindingType -> * where
    DataBinding :: Text -> ABinding 'Data
    StateBinding :: Text -> ABinding 'State

{-@ type NE a = {v:[a] | len v > 0}  @-}

{-@
data OutData :: BindingType -> Type where
    Direct :: ABinding b -> OutData b
    Destruct :: NE (OutData b) -> OutData b
@-}

data OutData :: BindingType -> Type where
    Direct :: ABinding b -> OutData b
    Destruct :: [OutData b] -> OutData b

If I append a deriving clause as follows:

data OutData :: BindingType -> Type where
    Direct :: ABinding b -> OutData b
    Destruct :: [OutData b] -> OutData b
    deriving (Show, Eq, Generic)

the type checker complains with:

> **** LIQUID: UNSAFE ************************************************************
> 
> error:
>     Liquid Type Mismatch
>     .
>     The inferred type
>       VV : {v : [(OutData a)] | v ~~ ?a
>                                               && len v >= 0
>                                               && v == ?a}
>     .
>     is not a subtype of the required type
>       VV : {VV : [(OutData a)] | len VV > 0}
>     .
>     in the context
>       ?a : (GHC.Generics.M1 (TYPE 'GHC.Types.LiftedRep) GHC.Generics.C ('GHC.Generics.MetaCons [GHC.Types.Char] 'GHC.Generics.PrefixI 'GHC.Types.False) (GHC.Generics.M1 (TYPE 'GHC.Types.LiftedRep) GHC.Generics.S ('GHC.Generics.MetaSel ('GHC.Maybe.Nothing GHC.Types.Symbol) 'GHC.Generics.NoSourceUnpackedness 'GHC.Generics.NoSourceStrictness 'GHC.Generics.DecidedLazy) (GHC.Generics.K1 (TYPE 'GHC.Types.LiftedRep) GHC.Generics.R [(OutData a)])) b)
>    |
>    | data OutData :: BindingType -> Type where
>    | ^

This looks like the situation where LH’s defaults cannot prove the termination of some code generated by GHC (I’m guessing the “derived” code).

I thought we had some flag to disable checking on compiler generated code, but if not I think we should add one!

For now you can either not do the deriving OR put the data definition in a separate module and put the —no-termination flag on that module?

On Thu, Nov 26, 2020 at 12:54 PM Sebastian notifications@github.com wrote:

The following GADT type checks just fine:

{-@ LIQUID "--exact-data-cons" @-} {-@ LIQUID "--prune-unsorted" @-} {-# LANGUAGE NoOverloadedLists #-} {-# LANGUAGE NoOverloadedStrings, DataKinds, KindSignatures, TypeApplications, GADTs #-} module Base where

import Prelude import Data.List.NonEmpty import Data.Text hiding (append)

data BindingType = State | Data

data ABinding :: BindingType -> * where DataBinding :: Text -> ABinding 'Data StateBinding :: Text -> ABinding 'State

{-@ type NE a = {v:[a] | len v > 0} @-}

{-@ data OutData :: BindingType -> Type where Direct :: ABinding b -> OutData b Destruct :: NE (OutData b) -> OutData b @-}

data OutData :: BindingType -> Type where Direct :: ABinding b -> OutData b Destruct :: [OutData b] -> OutData b

If I append a deriving clause as follows:

data OutData :: BindingType -> Type where Direct :: ABinding b -> OutData b Destruct :: [OutData b] -> OutData b deriving (Show, Eq, Generic)

the type checker complains with:

LIQUID: UNSAFE ****

error: Liquid Type Mismatch . The inferred type VV : {v : [(OutData a)] v ~~ ?a && len v >= 0 && v == ?a} . is not a subtype of the required type VV : {VV : [(OutData a)] len VV > 0} . in the context ?a : (GHC.Generics.M1 (TYPE 'GHC.Types.LiftedRep) GHC.Generics.C ('GHC.Generics.MetaCons [GHC.Types.Char] 'GHC.Generics.PrefixI 'GHC.Types.False) (GHC.Generics.M1 (TYPE 'GHC.Types.LiftedRep) GHC.Generics.S ('GHC.Generics.MetaSel ('GHC.Maybe.Nothing GHC.Types.Symbol) 'GHC.Generics.NoSourceUnpackedness 'GHC.Generics.NoSourceStrictness 'GHC.Generics.DecidedLazy) (GHC.Generics.K1 (TYPE 'GHC.Types.LiftedRep) GHC.Generics.R [(OutData a)])) b)

data OutData :: BindingType -> Type where

^

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1803__;!!Mih3wA!QH57VdReqyyp8cS-LDim46sGLM6xLpIzsCjU-aIOpwxqcpNQtOTl9JGEYZTjw8_6$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OD6G63XA32WXVPRFYDSR26AJANCNFSM4UEEZGZQ__;!!Mih3wA!QH57VdReqyyp8cS-LDim46sGLM6xLpIzsCjU-aIOpwxqcpNQtOTl9JGEYZcB8b4h$ .

ucsd-progsys / liquidhaskell

Refined GADTs with deriving confuse the type checker #1803