Custom type errors can be repeated
Summary
In some cases, exactly the same custom type error (text and source location) can be reported numerous times, sometimes filling multiple terminal windows.
Steps to reproduce
This is a fairly gentle simplification of something I encountered at work; I haven't attempted to reduce it properly. In the real code, the error is reported many, many times. The simplification doesn't quite get there. In GHC 9.2, the error is reported four times. In 9.4, it's reported three times.
{-# language AllowAmbiguousTypes #-}
{-# language DataKinds #-}
{-# language FunctionalDependencies #-}
{-# language PolyKinds #-}
{-# language StandaloneKindSignatures #-}
{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language TypeOperators #-}
{-# language UndecidableInstances #-}
module Borkborkbork where
import GHC.TypeLits hiding (Nat)
import qualified GHC.TypeLits as TL
infixr 5 ++
type (++) :: forall k. [k] -> [k] -> [k]
type family xs ++ ys where
'[] ++ ys = ys
(x : xs) ++ ys = x : xs ++ ys
data Nat = Z | S Nat
type ToNat :: TL.Nat -> Nat
type family ToNat n where
ToNat 0 = Z
ToNat n = S (ToNat (n - 1))
type Take :: forall k. Nat -> [k] -> [k]
type family Take n xs where
Take (S n) (x : xs) = x : Take n xs
Take _ _ = '[]
type Drop :: forall k. Nat -> [k] -> [k]
type family Drop n xs where
Drop (S n) (_ : xs) = Drop n xs
Drop _ xs = xs
type Tail :: forall k. [k] -> [k]
type family Tail xs where
Tail (_ : xs) = xs
Tail '[] = TypeError ('Text "Tail: empty list")
type FindIndicesOf :: forall k. k -> [k] -> [Nat]
type FindIndicesOf x xs = FindIndicesOf' Z x xs
type FindIndicesOf' :: forall k. Nat -> k -> [k] -> [Nat]
type family FindIndicesOf' n needle haystack where
FindIndicesOf' _n _needle '[] = '[]
FindIndicesOf' n needle (needle : haystack) = n : FindIndicesOf' (S n) needle haystack
FindIndicesOf' n needle (_ : haystack) = FindIndicesOf' (S n) needle haystack
type TheOnly :: forall k. ErrorMessage -> ErrorMessage -> [k] -> k
type family TheOnly empty_err many_err xs where
TheOnly empty_err _ '[] = TypeError empty_err
TheOnly _ _ '[x] = x
TheOnly _ many_err _ = TypeError many_err
type MyConstraint n dipinp dipout inp out =
( Drop n inp ~ dipinp
, Drop n out ~ dipout
, inp ~ (Take n inp ++ dipout)
, out ~ (Take n inp ++ dipout) )
class dipinp ~ (hddip : Tail dipinp)
=> Foom hddip dipinp dipout inp out
| hddip inp -> dipinp, hddip inp out -> dipout, hddip inp dipout -> out where
foom :: ()
instance ( n ~ TheOnly EmptyError ManyError (FindIndicesOf hddip inp)
, MyConstraint n dipinp dipout inp out
, dipinp ~ (hddip : tldip) ) => Foom hddip dipinp dipout inp out where
foom = ()
type EmptyError = Text "Feed me, Seymour. I'm hungry."
type ManyError = Text "I couldn't eat another bite."
bah :: ()
bah = foom @Int @[Int, Char, Bool] @'[] @[Char, Bool] @'[Nat]
Expected behavior
I expect the error to be reported exactly once.
Discussion
I imagine that the error gets reported every time the type checker bangs up against it for one reason or another. If it's too hard (or even impossible) to avoid running into the same error repeatedly, we should keep a set of hashes of custom type error/source location pairs (for each type checking SCC?), and only report an error if it hasn't been reported already. Optionally, we could count and report how many times each repeated error occurs, in case that's useful for something.
Environment
- GHC version used: 9.4.1
Optional:
- Operating System:
- System Architecture: