Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type level nat parameter causes LH to check less #2457

Open
kleinreact opened this issue Dec 4, 2024 · 10 comments
Open

Type level nat parameter causes LH to check less #2457

kleinreact opened this issue Dec 4, 2024 · 10 comments

Comments

@kleinreact
Copy link

kleinreact commented Dec 4, 2024

Lets say I wanna have a bounded number type with Num capabilities, then I can get that for some fixed lower bound 0 and upper bound 9 as follows:

{-@ LIQUID "" @-}

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

module T2457 where

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

{-@ type BI010 = { i : Integer | i >= 0 && i < 10 } @-}

{-@ data T = T BI010 @-}
type T :: Type
data T = T Integer

{-@ inline t2i @-}
{-@ t2i :: t : T -> { i : BI010 | t == T i } @-}
t2i :: T -> Integer
t2i (T i) = i
{-# INLINE t2i #-}

t0 :: T
t0 = T 3

-- does not LH type check, as expected
--t1 :: T
--t1 = T 10

{-@
instance Num T where
  (+) ::
    a : T ->
    { b : T | t2i a + t2i b < 10 } ->
    { t : T | t2i t == t2i a + t2i b }

  (-) ::
    a : T ->
    { b : T | t2i a >= t2i b } ->
    { t : T | t2i t == t2i a - t2i b }

  (*) ::
    a : T ->
    { b : T | t2i a * t2i b < 10 } ->
    { t : T | t2i t == t2i a * t2i b }

  negate :: T -> T
  abs    :: T -> T
  signum :: T -> T

  fromInteger ::
    i : BI010 ->
    { t : T | t2i t == i }
@-}
instance Num T where
  a + b        = T $ t2i a + t2i b
  a - b        = T $ t2i a - t2i b
  a * b        = T $ t2i a * t2i b
  negate       = undefined
  abs          = id
  signum       = undefined
  fromInteger  = T

t2 :: T
t2 = 3 + 3

-- does not LH type check, as expected
--t3 :: T
--t3 = 3 + 8

LH checks the bounds in this case as expected.

However, if I parameterize the bound using a type level natural instead, e.g.

{-@ LIQUID "" @-}

{-@ embed Natural as Int @-}
{-@ type BoundedInteger N = { i : Integer | N > 0 && i >= 0 && i < N } @-}

{-@ data P n = P Integer @-}
{-@ P :: forall (n :: Nat). BoundedInteger n -> P n @-}
type P :: Nat -> Type
data P n = P Integer

{-@ inline p2i @-}
{-@ p2i :: forall (n :: Nat). p : P n -> { i : BoundedInteger n | p == P i } @-}
p2i :: P n -> Integer
p2i (P i) = i
{-# INLINE p2i #-}

p0 :: P 10
p0 = P 3

-- does not LH type check, as expected
--p1 :: P 10
--p1 = P 10

{-@
instance Num (P n) where
  (+) ::
    forall (n :: Nat).
    a : P n ->
    { b : P n | p2i a + p2i b < n } ->
    { x : P n | p2i x == p2i a + p2i b }

  (-) ::
    forall (n :: Nat).
    a : P n ->
    { b : P n | p2i a >= p2i b } ->
    { x : P | p2i x == p2i a - p2i b }

  (*) ::
    forall (n :: Nat).
    a : P n ->
    { b : P n | p2i a * p2i b < n } ->
    { x : P | p2i x == p2i a * p2i b }

  negate :: forall (n :: Nat). P n -> P n
  abs    :: forall (n :: Nat). P n -> P n
  signum :: forall (n :: Nat). P n -> P n

  fromInteger ::
    forall (n :: Nat).
    i : BoundedInteger n ->
    { x : P n | p2i x == i }
@-}
instance Num (P n) where
  a + b        = P $ p2i a + p2i b
  a - b        = P $ p2i a - p2i b
  a * b        = P $ p2i a * p2i b
  negate       = undefined
  abs          = id
  signum       = undefined
  fromInteger  = P

p2 :: P 10
p2 = 3 + 3

-- LH SAFE, but 3 + 9 is no refinement in P 10!
p3 :: P 10
p3 = 3 + 9

then the last definition of p3 LH type checks, although it shouldn't. Note that only change here is the additionally introduced type level nat parameter.

I'd expect the parameterized version to behave the same as the non-parameterized one in this case.

Tested with GHC 9.10 and 8c550df.


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

@nikivazou
Copy link
Member

Hey @kleinreact! I cannot really run this code, because LH gives me too many errors before the p3...
But, this is in the direction you want:

{-# LANGUAGE DataKinds #-}

Concretely, the below seems correct for me (i.e., p2i and p2 are ok and p3 unsafe)

{-# 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 @-}


type P :: Nat -> Type
data P n = P Integer

{-@ P :: forall (n :: Nat). x:{Integer | x == n} -> {pp:P n |  n == x } @-}

{-@ p2i :: forall (n :: Nat). p : P n -> { i : Integer | i  == n  } @-}
p2i :: forall n. P n -> Integer
p2i (P i) = i

p2 :: P 10
p2 = P (2 + 8)

p3 :: P 10
p3 = P (3 + 9)

@kleinreact
Copy link
Author

I cannot really run this code, because LH gives me too many errors before the p3...

Oh, I'm sry, I should have added more context on my setup. Here's the options and imports that work for me:

{-@ LIQUID "" @-}

{-# LANGUAGE StandaloneKindSignatures #-}

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

{-@ LIQUID "--prune-unsorted" @-}

module Liquid.Test where

import Prelude

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

{-@ embed Natural as Int @-}
...

Concretely, the below seems correct for me (i.e., p2i and p2 are ok and p3 unsafe)

Yes, but in your case the Num instance is not used. It breaks for me as soon as I use the implicit fromInteger call added by GHC via using

p3 :: P 10
p3 = 3 + 9

instead of

p3 :: P 10
p3 = P (3 + 9)

That's exactly where the behavior differs between the T and P definitions given above.

@kleinreact
Copy link
Author

Thanks to @nikivazou we also got the reproducer working with 791567f. I updated the code above accordingly.

After the update the code now produces multiple

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

caused by using the Num instance inside the declaration of p3. Thus, it looks very much related to #2447 now.

@AlecsFerra
Copy link
Contributor

AlecsFerra commented Jan 14, 2025

Hi, now refining the return type of a data constructors is disallowed so @nikivazou 's code should be rejected.

@kleinreact is this what were you trying to achieve?

{-# LANGUAGE DataKinds #-}

module Fin where

import GHC.Base
import GHC.Num.Natural
import GHC.TypeNats

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

type Fin :: Nat -> Type
data Fin n where
{-@ MkFin :: forall (n :: Nat) . { i:Nat | i < n } -> Fin n @-}
    MkFin :: forall n . Int -> Fin n

{-@ unFin :: forall (n :: Nat) . Fin n -> { i:Nat | i < n } @-}
unFin :: forall n . Fin n -> Int
unFin (MkFin i) = i

p0 :: Fin 10
p0 = MkFin 3

p1 :: Fin 10
p1 = MkFin $ 3 + 3

{-@ fail p2 @-}
p2 :: Fin 10
p2 = MkFin $ 9 + 3

p2 fails to TC as expected

@kleinreact
Copy link
Author

@AlecsFerra yes that is basically what I want, but I need unFin inlined here such that I can use it in the Num instance later on.

However, adding a {-@ inline unFin @-} gives me a

   Illegal type specification for `Fin.unFin`
    Fin.unFin :: forall n .
                 lq_tmp$db##0:(Fin.Fin n) -> {VV : GHC.Types.Int | VV == lqdc##$select##Fin.MkFin##1 lq_tmp$db##0
                                                                   && VV >= 0
                                                                   && VV < n}
    Sort Error in Refinement: {VV : int | VV == lqdc##$select##Fin.MkFin##1 lq_tmp$db##0
                                          && VV >= 0
                                          && VV < n}
    Unbound symbol lqdc##$select##Fin.MkFin##1 --- perhaps you meant: Fin.MkFin ?
    Just
   |
26 | unFin (MkFin i) = i
   | ^^^

on 98c7729.

@AlecsFerra
Copy link
Contributor

AlecsFerra commented Jan 14, 2025

@AlecsFerra yes that is basically what I want, but I need unFin inlined here such that I can use it in the Num instance later on.

However, adding a {-@ inline unFin @-} gives me a

   Illegal type specification for `Fin.unFin`
    Fin.unFin :: forall n .
                 lq_tmp$db##0:(Fin.Fin n) -> {VV : GHC.Types.Int | VV == lqdc##$select##Fin.MkFin##1 lq_tmp$db##0
                                                                   && VV >= 0
                                                                   && VV < n}
    Sort Error in Refinement: {VV : int | VV == lqdc##$select##Fin.MkFin##1 lq_tmp$db##0
                                          && VV >= 0
                                          && VV < n}
    Unbound symbol lqdc##$select##Fin.MkFin##1 --- perhaps you meant: Fin.MkFin ?
    Just
   |
26 | unFin (MkFin i) = i
   | ^^^

on 98c7729.

You need to enable at least one of the flags that reflects selectors like --reflection

@kleinreact
Copy link
Author

I still get the same error, also after adding the --reflection flag.

@AlecsFerra
Copy link
Contributor

AlecsFerra commented Jan 14, 2025

Uhm super weird if instead of inline you use reflect unFin? Sorry I can't try it right now as I left my laptop at the office

@kleinreact
Copy link
Author

Using reflet unFin works, but the original code above declaring P then still gives me

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

after the introduction of p2, where I now changed the declaration of P to

type P :: Nat -> Type
data P n where
  {-@ P :: forall (n :: Nat). BoundedInteger n -> P n @-}
  P :: forall n. Integer -> P n

@AlecsFerra
Copy link
Contributor

Oh ok, now I understand the code is triggered by the usage of typeclass code, from what I know its not well tested/maintained #2434.

I don't know the specifics of how it works but I guess is has something to do with the dictionary resolution that is forgetting to bring in scope type parameters used as value

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants