ucsd-progsys/liquidhaskell

"Re-sugar" GHC.Types.: x GHC.Types.: GHC.Types.[] back into [x]?

Open

#2,229 建立於 2023年9月30日

在 GitHub 查看
 (1 留言) (1 反應) (0 負責人)Haskell (1,306 star) (157 fork)batch import
good first issue

描述

Type errors with lists are quite ugly:

λ :r
[1 of 1] Compiling MyLib            ( MyLib.hs, interpreted )

**** LIQUID: UNSAFE ************************************************************

MyLib.hs:42:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : [GHC.Types.Int] | v == MyLib.take' (GHC.Types.: (1 : int) (GHC.Types.: (2 : int) (GHC.Types.: (3 : int) (GHC.Types.: (4 : int) (GHC.Types.: (5 : int) GHC.Types.[]))))) (4 : int)
                                  && len v == MyLib.imin (GHC.Tuple.(,) (len (GHC.Types.: (1 : int) (GHC.Types.: (2 : int) (GHC.Types.: (3 : int) (GHC.Types.: (4 : int) (GHC.Types.: (5 : int) GHC.Types.[])))))) (4 : int))
                                  && len v >= 0}
    .
    is not a subtype of the required type
      VV : {VV : [GHC.Types.Int] | len VV == 5}
    .
    Constraint id 7
   |
42 | ex1 = take' [1,2,3,4,5] 4
   | ^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.

It would be nice if LH re-sugared those conses back into Haskell list syntax:

λ :r
[1 of 1] Compiling MyLib            ( MyLib.hs, interpreted )

**** LIQUID: UNSAFE ************************************************************

MyLib.hs:42:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : [GHC.Types.Int] | v == MyLib.take' [(1 : int), (2 : int), (3 : int), (4 : int), (5 : int)] (4 : int)
                                  && len v == MyLib.imin (GHC.Tuple.(,) [(1 : int), (2 : int), (3 : int), (4 : int), (5 : int)] (4 : int))
                                  && len v >= 0}
    .
    is not a subtype of the required type
      VV : {VV : [GHC.Types.Int] | len VV == 5}
    .
    Constraint id 7
   |
42 | ex1 = take' [1,2,3,4,5] 4
   | ^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.

貢獻者指南