Skip to content

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:
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information