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

[ramirez7]

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.

[facundominguez]

To avoid confusion, the error message should probably use syntax that can be accepted by the parser of LH. In this way, the ticket is connected to #2193.