Simplify constraints when showing errors / typed holes
Motivation
I'm doing some type-level programming with typed holes, and often I will see constraints of the form x ~ (y : ys)
or
(x : xs) ~ (y : ys)
.
There can be several such constraints that form a "chain", and it would be an immense
help if they were simplified, such that redundant variables wouldn't be shown,
e.g. x :: a
when we have the constraint a ~ Int
.
Proposal
Apply constraints before showing the information.
Example
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE GADTs #-}
{-# OPTIONS_GHC -fno-show-valid-hole-fits #-}
data IsInt a where
IsInt :: IsInt Int
f :: IsInt a -> a -> Int
f IsInt x = _
This currently shows (with GHC 9.2.4)
X.hs:9:13: error:
• Found hole: _ :: Int
• In an equation for ‘f’: f IsInt x = _
• Relevant bindings include
x :: a (bound at X.hs:9:9)
f :: IsInt a -> a -> Int (bound at X.hs:9:1)
Constraints include a ~ Int (from X.hs:9:3-7)
|
9 | f IsInt x = _
| ^
It should show
X.hs:9:13: error:
• Found hole: _ :: Int
• In an equation for ‘f’: f IsInt x = _
• Relevant bindings include
x :: Int (bound at X.hs:9:9)
f :: IsInt a -> a -> Int (bound at X.hs:9:1)
|
9 | f IsInt x = _
| ^