ucsd-progsys/liquidhaskell
Voir sur GitHub"Re-sugar" GHC.Types.: x GHC.Types.: GHC.Types.[] back into [x]?
Open
#2 229 ouverte le 30 sept. 2023
good first issue
Métriques du dépôt
- Stars
- (1 306 stars)
- Métriques de merge PR
- (Merge moyen 2j 18h) (12 PRs mergées en 30 j)
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.