ucsd-progsys/liquidhaskell

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

Open

#2,229 opened on Sep 30, 2023

View on GitHub
 (1 comment) (1 reaction) (0 assignees)Haskell (157 forks)batch import
good first issue

Repository metrics

Stars
 (1,306 stars)
PR merge metrics
 (Avg merge 2d 18h) (12 merged PRs in 30d)

Description

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.

Contributor guide