Empty data types depending on type literals don't behave as expected

[kleinreact]

I wanna make use of some dependently uninhabited data types, where the following references the expected behavior

{-@ LIQUID "" @-}

{-@ data Empty = Empty ({ _ : Int | false }) @-}
data Empty = Empty Int

-- some = Empty 0  -- < rejected for any v : Int

-- accepted: as the error is liquid unreachable
getSome :: Empty -> Int
getSome (Empty _) = error ""

However, if I parameterize the above with a type natural, then false detection stops working in the uninhabited case

{-@ LIQUID "" @-}

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
{-# OPTIONS_GHC -fno-warn-unused-imports #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}

module T2447 where

import GHC.Base (Type)
import GHC.TypeNats (Nat, Natural)

{-@ embed Natural as Int @-}

{-@ type FalseIfZero N = { i : Int | N /= 0 } @-}
{-@ data EmptyIfZero n = EmptyIfZero Int @-}
{-@ EmptyIfZero :: forall (n :: Nat). FalseIfZero n -> EmptyIfZero n @-}
type EmptyIfZero :: Nat -> Type
data EmptyIfZero n = EmptyIfZero !Int

someNonZeroT :: EmptyIfZero 1
someNonZeroT = EmptyIfZero 0  -- < accepted for any v : Int
                              -- as long as the type parameter is not 0

-- someZeroT :: EmptyIfZero 0
-- someZeroT = EmptyIfZero 0  -- rejected for any v : Int

-- HOWEVER!!
-- rejected: although the error is still liquid unreachable
getSomeZeroT :: EmptyIfZero 0 -> Int
getSomeZeroT (EmptyIfZero _) = error ""

---

It also gives me a

**** LIQUID: ERROR *************************************************************
<no location info>: error:
    :1:1-1:1: Error
  Constraint with free vars
  1
  [n]
  Try using the --prune-unsorted flag

for getSomeZeroT unless I enable --prune-unsorted, which might be related, I guess.

---

2024-12-17: Update of the reproducer to work with 791567f.

[nikivazou]

Hey, for the error I will have to take a deeper look to fix it (the literal 0 assumes the n but it does not really into the typing environment in the case split, because data constructors currently do not insert type level binders).

The, it is this ! in the data definition that cancels out all the infos (maybe you know more how it works than me).

Like in #2457 LH can relate the type variable with the value parameter only by the information you specify in the data constructor signature. So, the following has some behavior close to the one I expect you want it to have

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

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
module Fixme where
import GHC.Base (Type)
import GHC.TypeNats (Nat, Natural)
import GHC.Num.Natural (Natural)

{-@ embed  GHC.Num.Natural.Natural as int @-}
{-@ embed Natural as Int @-}


type EmptyIfZero :: Nat -> Type
data EmptyIfZero n = EmptyIfZero Int

{-@ EmptyIfZero :: forall (n :: Nat). x:{Int | x /= 0 } 
                -> {pp:EmptyIfZero n  |  n == x } @-}

someNonZeroT :: EmptyIfZero 1
someNonZeroT = EmptyIfZero 0  -- < accepted for any v : Int
                              -- as long as the type parameter is not 0

someZeroT :: EmptyIfZero 0
someZeroT = EmptyIfZero 0  -- rejected for any v : Int

someZeroT2 :: EmptyIfZero 13
someZeroT2 = EmptyIfZero 12  -- rejected for any v : Int

getSomeZeroT :: EmptyIfZero n -> Int
getSomeZeroT (EmptyIfZero 0) = error ""
getSomeZeroT (EmptyIfZero n) = n

[kleinreact]

The, it is this ! in the data definition that cancels out all the infos (maybe you know more how it works than me).

Interesting observation. I wasn't aware of that and no, I don't have any knowledge of how StrictData works under the hood.

So, the following has some behavior close to the one I expect you want it to have

No, I don't like to error in the term literal 0-case, but when the type literal is zero, which is equivalent to the uninhabited type here.

Your modification also does not LH type check for me. It complains about the declaration of someNonZeroT

   Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Types.Int | v == ?b
                                && v == GHC.Types.I# 0
                                && v == (0 : int)}
    .
    is not a subtype of the required type
      VV : {VV##1532 : GHC.Types.Int | VV##1532 /= 0}
    .
    in the context
      ?b : {?b : GHC.Types.Int | ?b == GHC.Types.I# 0
                                 && ?b == (0 : int)}
    Constraint id 23
   |
24 | someNonZeroT = EmptyIfZero 0  -- < accepted for any v : Int
   |                            ^