Cannot create spec for Array#

[andrewthad]

With a module of:

{-# language MagicHash #-}                                                                           

module MySpec
  ( Array#
  , indexArray#                                                                                      
  ) where

import GHC.Exts (Array#,indexArray#)                                                                 

and a specification of:

module spec MySpec where                                                                             

import GHC.Base                                                                                      

data variance MySpec.Array# covariant                                                                

indexArray# :: forall a. x:(MySpec.Array# a) -> {v:Nat | v < len x } -> a                            

This fails with:

src/MySpec.spec:7:1: error:
    • Unknown variable `MySpec.indexArray#`
    rawTySigs
    • 
  |
7 | indexArray# :: forall a. x:(MySpec.Array# a) -> {v:Nat | v < len x } -> a 
  | ^^^^^^^^^^^^

Importing GHC.Exts in addition to GHC.Base does not improve this. I'm not sure if this fails because liquid haskell doesn't like names with hash (it seems to lex correctly though) or if there is something problematic about importing binders from ghc-prim modules.

[ranjitjhala]

Hmm, can you try to replace (MySpec.Array# a) with a hole _ ? So change the signature to

indexArray# :: forall a. x:_ -> {v:Nat | v < len x } -> a

[andrewthad]

As:

indexArray# :: forall a. x:_ -> {v:Nat | v < len x } -> a

It still errors with

Unknown variable `MySpec.indexArray#`

[andrewthad]

Also, I'm using liquidhaskell as a GHC plugin, not the old way, if that matters.

[ranjitjhala]

Hmm pretty sure I’ve written specs with # … let me check

On Mon, Feb 14, 2022 at 10:05 AM Andrew Martin @.***> wrote:

Also, I'm using liquidhaskell as a GHC plugin, not the old way, if that matters.

— Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1936-23issuecomment-2D1039391444&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=7slH4IxvfzqH1S1s9teRQmVc3ezq2iY7cWziVXlDtGKdT0uR-4dQKUHctCMPl9_k&s=NAEFXZf_R-6_bJVx5VwYaBZVB_R-871eiZAa5PfomA4&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OAPJ2WMNUBZQ32XAGLU3E77NANCNFSM5OME3YAA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=7slH4IxvfzqH1S1s9teRQmVc3ezq2iY7cWziVXlDtGKdT0uR-4dQKUHctCMPl9_k&s=oxqgFvre7oV-aEytNWAX8K5LkhwD_Q6713yLm5HOQNg&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=7slH4IxvfzqH1S1s9teRQmVc3ezq2iY7cWziVXlDtGKdT0uR-4dQKUHctCMPl9_k&s=LQ4RY_XRTA6Nry8p85PLdun8pY5gTAUxPTjWzmrMwQ0&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=7slH4IxvfzqH1S1s9teRQmVc3ezq2iY7cWziVXlDtGKdT0uR-4dQKUHctCMPl9_k&s=cuoX9WwQ3OPw33VJS7fe9SRNH_JmAzRgrIrsfkOJr7U&e=.

You are receiving this because you commented.Message ID: @.***>

[andrewthad]

You're right. I just found GHC.CString.spec. The trick is that LH does something strange with module scope and reexports. I had to use GHC.Prim.indexArray# (and the same for Array#). Even without explicitly importing GHC.Prim, this is allowed.

[andrewthad]

But the LH spec parser does not like unboxed tuples, so it then fails on:

GHC.Prim.indexArray# :: forall a. x:(GHC.Prim.Array# a) -> {v:Int# | v >= 0} -> (# a #)

with:

Error when parsing  src/MySpec.spec : src/MySpec.spec:7:82:
  |
7 | GHC.Prim.indexArray# :: forall a. x:(GHC.Prim.Array# a) -> {v:Int# | v >= 0} -> (# a #)
  |                                                                                  ^
unexpected '#'
expecting ')', btP, or lowerIdP

I may be able to fix this though.

[andrewthad]

Impressively, LH understands this spec:

GHC.Prim.indexIntArray# :: forall a. x:GHC.Prim.ByteArray# -> {v:GHC.Prim.Int# | v >= 0} -> GHC.Prim.Int#

And then even more impressively, LH understands all the unlifted arithmetic operations:

{-# language MagicHash #-}                                                                           

module Tester                                                                                        
  ( foo                                                                                              
  ) where                                                                                            

import MySpec                                                                                        
import GHC.Exts                                                                                      

foo :: Int# -> ByteArray# -> Int#                                                                    
foo ix arr = case ix >=# 0# of                                                                       
  1# -> indexIntArray# arr ix                                                                        
  _ -> 0#                                                                                            

That is accepted by LH, which surprised me.