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 (1,306 stars) (157 forks)batch import
good first issue

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

Tech stack
None
Domain
developer experiencetooling
Issue type
feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-2 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
stale
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
clear
Prerequisites
Liquid Haskell internal error printing
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
20
Research direction
The issue requests that Liquid Haskell re sugar the GHC internal representation of list literals (e.g., GHC.Types.: and GHC.Types.[]) back into standard Haskell list syntax (e.g., [1..]) in type error messages. To implement this, locate the code responsible for rendering refinement types, likely in the 'Liquid' or 'Language' directory. Look for functions that convert internal term representations to strings, and add a case to recognize list cons and nil constructors and print them as [x, y, z] or [x..] as appropriate. The maintainer's comment (if any) could provide guidance; currently there is only one comment from the original poster.
"Re-sugar" GHC.Types.: x GHC.Types.: GHC.Types.[] back into [x]? · ucsd-progsys/liquidhaskell#2229 | Good First Issue