GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-08-15T13:33:00Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/23817Improve the reporting of an ambiguous ErrorMessage2023-08-15T13:33:00Zsheafsam.derbyshire@gmail.comImprove the reporting of an ambiguous ErrorMessageWhen there is an ambiguous error message, e.g.
```haskell
-- Example using TypeError
type family F msg where { F msg = TypeError msg }
foo :: F msg => ()
foo = ()
bar = foo
--------------------
-- Example using Unsatisfiable
baz :: ()
...When there is an ambiguous error message, e.g.
```haskell
-- Example using TypeError
type family F msg where { F msg = TypeError msg }
foo :: F msg => ()
foo = ()
bar = foo
--------------------
-- Example using Unsatisfiable
baz :: ()
baz = unsatisfiable
```
We get an error message that looks like
```
error: [GHC-22250]
- msg0
```
with the ambiguous metavariable `msg0` appearing in the message.
We might instead want to default this metavariable to get a more sensible error message. cc @adamgundry who observed this.
This wouldn't handle all situations, e.g.
```haskell
type family F ty where { F ty = TypeError ( Text "Message header" :$$: ShowType ty ) }
foo' :: F ty => ()
foo' = ()
bar' = foo'
```
```
error:
* Message header
ty0
```
and now `ty0 :: Type` which we don't really have a good way of defaulting. But perhaps that's OK.
Another alternative would be to avoid reporting it using the usual mechanism entirely, as @monoidal suggests in https://gitlab.haskell.org/ghc/ghc/-/issues/23817#note_520095.https://gitlab.haskell.org/ghc/ghc/-/issues/23438`TypeError` thrown in standalone `via` deriving but not attached `via` deriving2023-05-31T18:33:03Zparsonsmatt`TypeError` thrown in standalone `via` deriving but not attached `via` deriving## Summary
A `newtype` for `via` deriving is provided that gives a `TypeError`, effectively banning the instance from use, but with a nice error message. We use this at work to prevent folks from running database operations in the "main...## Summary
A `newtype` for `via` deriving is provided that gives a `TypeError`, effectively banning the instance from use, but with a nice error message. We use this at work to prevent folks from running database operations in the "main" monad, and instead guide them towards `runDB` which handles transactions.
## Steps to reproduce
```haskell
{-# language DerivingVia #-}
{-# language DataKinds #-}
{-# language UndecidableInstances #-}
{-# language StandaloneDeriving #-}
module Woops where
import GHC.TypeLits
class C a where
f :: a -> a
newtype Can'tBeC a = Can'tBeC a
instance ( TypeError ('Text "No")) => C (Can'tBeC a) where
f = error "unreachable"
instance C Int where f = id
data Good = Good
deriving C via (Can'tBeC Good)
data Bad = Bad
deriving via Can'tBeC Bad instance C Bad
```
With GHC 9.6.1, I get the following result:
```
λ ~/Projects/ghc-woops/ master* cabal build
Build profile: -w ghc-9.6.1 -O1
In order, the following will be built (use -v for more details):
- ghc-woops-0.1.0.0 (lib) (file src/Woops.hs changed)
Preprocessing library for ghc-woops-0.1.0.0..
Building library for ghc-woops-0.1.0.0..
[2 of 2] Compiling Woops ( src/Woops.hs, /home/matt/Projects/ghc-woops/dist-newstyle/build/x86_64-linux/ghc-9.6.1/ghc-woops-0.1.0.0/build/Woops.o, /
home/matt/Projects/ghc-woops/dist-newstyle/build/x86_64-linux/ghc-9.6.1/ghc-woops-0.1.0.0/build/Woops.dyn_o ) [Source file changed]
src/Woops.hs:25:1: error: [GHC-64725]
• No
• In the third argument of ‘ghc-prim-0.10.0:GHC.Prim.coerce’, namely
‘(f @(Can'tBeC Bad))’
In the expression:
ghc-prim-0.10.0:GHC.Prim.coerce
@(Can'tBeC Bad -> Can'tBeC Bad) @(Bad -> Bad) (f @(Can'tBeC Bad))
In an equation for ‘f’:
f = ghc-prim-0.10.0:GHC.Prim.coerce
@(Can'tBeC Bad -> Can'tBeC Bad) @(Bad -> Bad) (f @(Can'tBeC Bad))
When typechecking the code for ‘f’
in a derived instance for ‘C Bad’:
To see the code I am typechecking, use -ddump-deriv
|
25 | deriving via Can'tBeC Bad instance C Bad
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is consistent going back to GHC 8.10.7.
## Expected behavior
I expect that the `StandaloneDeriving` and attached deriving have the same behavior.
But, to be totally specific, I do want both instances to be *accepted*. The purpose of providing the `TypeError` instance here is to provide helpful error messages to folks that are using these, so instead of seeing `No instance for C Bad` they see `You need to do X if you want to use C in the Bad type` or similar.
## Environment
* GHC version used: 9.6.1, 9.4.5, 9.2.7, 8.10.7
Optional:
* Operating System: Ubuntu
* System Architecture: x86sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/22139TypeError's interaction with type family injectivity2022-09-02T20:55:29ZGergő ÉrdiTypeError's interaction with type family injectivityLet's say I have the following Haskell code, using `TypeFamilyDependencies`:
```haskell
data FieldK
data Field (f :: FieldK)
type family FieldToFieldKList (fs :: [Type]) = (r :: [FieldK]) | r -> fs where
FieldToFieldKList '[] = '[]...Let's say I have the following Haskell code, using `TypeFamilyDependencies`:
```haskell
data FieldK
data Field (f :: FieldK)
type family FieldToFieldKList (fs :: [Type]) = (r :: [FieldK]) | r -> fs where
FieldToFieldKList '[] = '[]
FieldToFieldKList (Field f : fs) = f : FieldToFieldKList fs
FieldToFieldKList (a : fs) = TypeError (Text "Must be a Field: " :<>: ShowType a)
```
This is currently thrice rejected by GHC:
* `TypeError` is a type family, and injective type family equations cannot have type family applications on their right-hand side (*Verifying injectivity annotation* note, check 3)
* Type variables `a` and `fs` of `a : fs` cannot be inferred from the right-hand side `TypeError ...`. (check 4)
* Overlap between the right-hand sides `[]` and `TypeError ...`, because type family applications pre-unify with everything (check B2)
Without the third (the `TypeError`) clause, GHC accepts this type family definition as injective.
My question is whether these three rejection reasons can be alleviated by the fact that the RHS in question is a `TypeError`. The idea being, if somewhere inside a type we arrive at a `TypeError _`, this will lead to a type error anyway, so we won't try to solve any further type equations. So it shouldn't cause any problems if we could derive inconsistent equations from type family applications that reduce to `TypeError _`.https://gitlab.haskell.org/ghc/ghc/-/issues/22126Custom type errors can be repeated2022-08-30T13:51:58ZDavid FeuerCustom 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 som...## 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.
```haskell
{-# 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:ZubinZubinhttps://gitlab.haskell.org/ghc/ghc/-/issues/21151Insoluble constraints arising from an ambiguity check are reported poorly2022-11-21T19:58:48Zsheafsam.derbyshire@gmail.comInsoluble constraints arising from an ambiguity check are reported poorlyThe way GHC reports insoluble constraints arising from an ambiguity check seems rather poor, as I discovered in #21149.
Example 1: an insoluble equality constraint.
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}...The way GHC reports insoluble constraints arising from an ambiguity check seems rather poor, as I discovered in #21149.
Example 1: an insoluble equality constraint.
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind ( Type )
class C (a :: Type)
instance ( Maybe w ~ Bool ) => C ()
```
```
error:
* Couldn't match type `Maybe w0' with `Bool'
Expected: forall w. ((Maybe w :: *) ~ (Bool :: *)) => C ()
Actual: forall w. ((Maybe w :: *) ~ (Bool :: *)) => C ()
* In the ambiguity check for an instance declaration
In the instance declaration for `C ()'
|
8 | instance ( Maybe w ~ Bool ) => C ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Note the strange `Expected`/`Actual` message which makes no sense.
------
By the way: this program is accepted if one doesn't enable `-XUndecidableInstances`, as the ambiguity check appears to be skipped altogether in that case. This seems to be due to the following code in `checkValidInstance`:
```haskell
-- Note that the Termination Condition is *more conservative* than
-- the checkAmbiguity test we do on other type signatures
-- e.g. Bar a => Bar Int is ambiguous, but it also fails
-- the termination condition, because 'a' appears more often
-- in the constraint than in the head
; undecidable_ok <- xoptM LangExt.UndecidableInstances
; if undecidable_ok
then checkAmbiguity ctxt ty
else checkInstTermination theta tau
```
This seems to be an example where `checkInstTermination` is not stricter than `checkAmbiguity`.
------
Example 2: an insoluble custom type error.
```haskell
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind ( Type )
import GHC.TypeLits ( TypeError, ErrorMessage(..) )
class C (a :: Type)
instance TypeError ( ShowType w ) => C ()
```
```
error:
* w0
* In the ambiguity check for an instance declaration
In the instance declaration for `C ()'
|
9 | instance TypeError ( ShowType w ) => C ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
I think these error messages are quite confusing. I think it would be better to adjust the way we report unsolved constraints arising from an ambiguity check to make it a bit clearer.
(The issue with `TypeError` was introduced in 9.3, as we used to not consider a type error to be insoluble and thus would allow it to go unsolved in an ambiguity check with `-XAllowAmbiguousTypes`.)sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/19858GADTs/existentials can hide values with custom type errors2022-02-24T10:00:53ZManuel BärenzGADTs/existentials can hide values with custom type errors## Summary
In GADTs, you can construct nested values where the inner values should not be constructable due to custom type errors.
## Steps to reproduce
We can define a type family containing a type error:
```haskell
type family OhNo...## Summary
In GADTs, you can construct nested values where the inner values should not be constructable due to custom type errors.
## Steps to reproduce
We can define a type family containing a type error:
```haskell
type family OhNo where
OhNo = TypeError (Text "Oh no")
```
We can define a GADT parametrised by this type error:
```haskell
data Bar (k :: b) where
Bar :: Bar OhNo
deriving instance Show (Bar k)
```
We get an error that no value `Bar` can be constructed due to the error:
```
*Main> Bar
<interactive>:23:1: error:
• Oh no
• When checking the inferred type
it :: forall b. Bar (TypeError ...)
```
But we can hide the type error as an existential:
```haskell
data SomeBar where
SomeBar :: Bar k -> SomeBar
deriving instance Show SomeBar
```
```
*Main> SomeBar Bar
SomeBar Bar
```
## Expected behavior
I would have expected the expression `SomeBar Bar` not to be well-typed. The custom type error should have been triggered.
## Environment
* GHC version used: 8.10.4https://gitlab.haskell.org/ghc/ghc/-/issues/18978Allow users to define an error message that is displayed when a constraint ca...2021-08-03T21:53:40Zsheafsam.derbyshire@gmail.comAllow users to define an error message that is displayed when a constraint can't be solvedI would like to enable users to annotate constraints with custom error messages; such a message would be displayed by GHC in the case that an annotated constraint could not be satisfied.
That is, I propose a special type family:
``...I would like to enable users to annotate constraints with custom error messages; such a message would be displayed by GHC in the case that an annotated constraint could not be satisfied.
That is, I propose a special type family:
```haskell
type Annotate :: ErrorMessage -> Constraint -> Constraint
```
Minimal illustration of the functionality:
```haskell
type F :: Type -> Constraint
type family F x where
F (a,b) = Annotate ( Text "F needs pair components to have the same type" ) ( a ~ b )
f :: F a => ()
f = ()
g :: ()
g = f @(Int, Bool)
```
would produce the error message:
```
* F needs pair components to have the same type
* Arising from a use of `f'
* In the expression: f @(Int, Bool)
In an equation for `g': g = f @(Int, Bool)
|
13 | g = f @(Int, Bool)
| ^^^^^^^^^^^^^^
````
instead of the decidably less helpful:
```
* Couldn't match type `Int' with `Bool' arising from a use of `f'
* In the expression: f @(Int, Bool)
In an equation for `g': g = f @(Int, Bool)
|
13 | g = f @(Int, Bool)
| ^^^^^^^^^^^^^^
```
I think this would be generally useful. For instance, one of my use cases is as follows: I have written a graphics shader library which uses type families to validate programs. When a user tries to read from an image or sample from a texture, we validate the operation using the image properties (available at the type level) as well as the arguments to the image operation that the user has provided (see [here](https://gitlab.com/sheaf/fir/-/blob/a6cb637f33b58653f6eb767c6964bab619472a73/src/FIR/Validation/Images.hs#L116)). This works well when the type family computation directly hits an error message, but can result in confusing messages when the type family application computes to another constraint. For instance, I have a constraint of the form
```haskell
type family TypeMatchesFormat (fmt :: ImageFormat) (a :: Type) :: Constraint where
MatchesFormat IntegralFormat a = Integral a
MatchesFormat FloatingFormat a = Floating a
MatchesFormat UnknownFormat _ = TypeError (Text "Unknown image format")
```
This leads to error messages of the form `Could not deduce Floating Word32` that are rather inscrutable, whereas with `Annotate` I could write:
```haskell
type family TypeMatchesFormat (fmt :: ImageFormat) (a :: Type) :: Constraint where
MatchesFormat IntegralFormat a = Annotate ( Text "Cannot use non-integral type " :<>: ShowType a :<>: Text " with an integral image format" ) ( Integral a )
MatchesFormat FloatingFormat a = Annotate ( Text "Cannot use non-float type " :<>: ShowType a :<>: Text " with a floating-point image format" ) ( Floating a )
MatchesFormat UnknownFormat _ = TypeError (Text "Unknown image format")
```https://gitlab.haskell.org/ghc/ghc/-/issues/18766TypeError and GADT pattern matching exhaustiveness2021-08-16T14:04:29ZZiyang Liuunsafefixio@gmail.comTypeError and GADT pattern matching exhaustiveness```haskell
data D a where
C1 :: D Int
C2 :: D Char
type family Elem x list where
Elem x '[] = 'False
Elem x (x ': as) = 'True
Elem x (y ': as) = Elem x as
foo :: Elem a '[Int] ~ 'True => D a -> ()
foo C1 = ()
```
Here...```haskell
data D a where
C1 :: D Int
C2 :: D Char
type family Elem x list where
Elem x '[] = 'False
Elem x (x ': as) = 'True
Elem x (y ': as) = Elem x as
foo :: Elem a '[Int] ~ 'True => D a -> ()
foo C1 = ()
```
Here GHC correctly determines that the pattern matching is exhaustive.
But if the first case of the type family is changed to
```haskell
Elem x '[] = TypeError ('Text "oops")
```
then GHC no longer thinks it's exhaustive.
This seems to be the case with any empty type family, not just `TypeError`.
This makes it hard if not impossible to customize type error messages.
## Environment
* GHC version used: 8.10.2https://gitlab.haskell.org/ghc/ghc/-/issues/17168Custom TypeError should include "arising from" clause2020-01-23T19:43:04ZAdam GundryCustom TypeError should include "arising from" clauseWhen a class constraint cannot be solved, the "No instance" message includes "arising from..." to specify the source of the constraint. However, if a custom type error is used to change the message, there is no "arising from..." clause. ...When a class constraint cannot be solved, the "No instance" message includes "arising from..." to specify the source of the constraint. However, if a custom type error is used to change the message, there is no "arising from..." clause. In complicated cases where the expression is large, this clause is useful in pinpointing the source of the error, so it would be helpful to include it.
For example, consider the following module:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
module CustomTypeError where
import GHC.TypeLits
class C a where
(%) :: a -> a -> a
instance TypeError (Text "No, Int cannot be a C") => C Int
foo = 2 % 3 :: Int
bar = 'a' % 'b' :: Char
```
This results in the following output:
```hs
CustomTypeError.hs:13:7: error:
• No, Int cannot be a C
• In the expression: 2 % 3 :: Int
In an equation for ‘foo’: foo = 2 % 3 :: Int
|
13 | foo = 2 % 3 :: Int
| ^^^^^
CustomTypeError.hs:15:7: error:
• No instance for (C Char) arising from a use of ‘%’
• In the expression: 'a' % 'b' :: Char
In an equation for ‘bar’: bar = 'a' % 'b' :: Char
|
15 | bar = 'a' % 'b' :: Char
| ^^^^^^^^^
```https://gitlab.haskell.org/ghc/ghc/-/issues/17027User defined Type Warnings2022-01-05T15:14:14ZAndreas KlebingerUser defined Type Warnings## Motivation
GHC Allows users to specify custom type errors for type level literals.
`type family TypeError (a :: ErrorMessage) :: b where ...`
This is obviously useful. For example in the listed example:
```
type family ByteSize x ...## Motivation
GHC Allows users to specify custom type errors for type level literals.
`type family TypeError (a :: ErrorMessage) :: b where ...`
This is obviously useful. For example in the listed example:
```
type family ByteSize x where
ByteSize Word16 = 2
ByteSize Word8 = 1
ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
Text " is not exportable.")
```
What about the reverse? If we want to go from bytes to types we could use.
```haskell
type family FitsIn x where
FitsIn 0 = ()
FitsIn 1 = Word8
...
FitsIn a = TypeWarning (Text "The byte size " :<>: ShowType a :<>:
Text " is defaulted to Integer.")
Integer
```
This would warn users in a similar fashion to how GHC warns about defaulting literals to Integers.
## Proposal
Add TypeWarning:
```haskell
type family TypeWarning (a :: ErrorMessage) b :: b where ...
```
I will not be implementing this (anytime soon at least) and it might need a ghc-proposal. But seems like an obvious idea.https://gitlab.haskell.org/ghc/ghc/-/issues/16894TypeError hides a second error message2020-01-23T19:40:11ZJoey HessTypeError hides a second error message# Summary
Using TypeError seems to hide other type error messages due to eg, bad arguments passed to a function.
# Steps to reproduce
Load into ghci:
```
{-# LANGUAGE DataKinds, UndecidableInstances, TypeFamilies #-}
import...# Summary
Using TypeError seems to hide other type error messages due to eg, bad arguments passed to a function.
# Steps to reproduce
Load into ghci:
```
{-# LANGUAGE DataKinds, UndecidableInstances, TypeFamilies #-}
import GHC.TypeLits
type family Check x :: Bool where
Check 'True = 'True
Check x = 'False
foo :: Check 'False ~ 'True => Int -> String
foo n = "never reached"
type family Check2 x :: Bool where
Check2 'True = 'True
Check2 x = TypeError ('Text "no")
foo2 :: Check2 'False ~ 'True => Int -> String
foo2 n = "never reached"
```
```
ghci> foo "bar"
<interactive>:69:1: error:
• Couldn't match type ‘'False’ with ‘'True’
arising from a use of ‘foo’
• In the expression: foo "bar"
In an equation for ‘it’: it = foo "bar"
<interactive>:69:5: error:
• Couldn't match expected type ‘Int’ with actual type ‘[Char]’
• In the first argument of ‘foo’, namely ‘"bar"’
In the expression: foo "bar"
In an equation for ‘it’: it = foo "bar"
ghci> foo2 "bar"
<interactive>:70:1: error:
• no
• In the expression: foo2 "bar"
In an equation for ‘it’: it = foo2 "bar"
```
# Expected behavior
I expected to see the same error about Int vs [Char] for foo2 as is shown for foo, as well as the custom TypeError. However, the use of TypeError somehow prevents the Int vs [Char] error from being displayed.
This is preventing me from using TypeError in situations where there might be another, more basic
type error in the same code.
This may be related to https://gitlab.haskell.org/ghc/ghc/issues/14771
# Environment
* GHC version used: 8.4.4, 8.6.5https://gitlab.haskell.org/ghc/ghc/-/issues/14771TypeError reported too eagerly2021-12-17T15:02:30ZSylvain HenryTypeError reported too eagerlyConsider the following example:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
impor...Consider the following example:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits
import Data.Proxy
data DUMMY
type family If c t e where
If True t e = t
If False t e = e
type family F (n :: Nat) where
--F n = If (n <=? 8) Int (TypeError (Text "ERROR"))
F n = If (n <=? 8) Int DUMMY
test :: (F n ~ Word) => Proxy n -> Int
test _ = 2
test2 :: Proxy (n :: Nat) -> Int
test2 p = test p
main :: IO ()
main = do
print (test2 (Proxy :: Proxy 5))
```
The type error is useful:
```
Bug.hs:26:11: error:
• Couldn't match type ‘If (n <=? 8) Int DUMMY’ with ‘Word’
arising from a use of ‘test’
• In the expression: test p
In an equation for ‘test2’: test2 p = test p
• Relevant bindings include
p :: Proxy n (bound at Bug.hs:26:7)
test2 :: Proxy n -> Int (bound at Bug.hs:26:1)
|
26 | test2 p = test p
| ^^^^^^
```
Now if we use the commented implementation of `F` (using `TypeError`), with GHC 8.2.2 and 8.0.2 we get:
```
Bug.hs:26:11: error:
• ERROR
• In the expression: test p
In an equation for ‘test2’: test2 p = test p
|
26 | test2 p = test p
| ^^^^^^
```
While with GHC 8.0.1 we get:
```
/home/hsyl20/tmp/Bug.hs:29:11: error:
• Couldn't match type ‘If (n <=? 8) Int (TypeError ...)’
with ‘Word’
arising from a use of ‘test’
• In the expression: test p
In an equation for ‘test2’: test2 p = test p
```
1) Could we restore the behavior of GHC 8.0.1?
2) In my real code, when I use DUMMY I get:
```
• Couldn't match type ‘If (n <=? 8) Int8 DUMMY’ with ‘Word’
Expected type: Word
Actual type: F n
```
If we could get the same report (mentioning the "Actual type") when we use `TypeError` that would be great.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeError reported too eagerly","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following example:\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\n\r\nimport GHC.TypeLits\r\nimport Data.Proxy\r\n\r\ndata DUMMY\r\n\r\ntype family If c t e where\r\n If True t e = t\r\n If False t e = e\r\n\r\n\r\ntype family F (n :: Nat) where\r\n --F n = If (n <=? 8) Int (TypeError (Text \"ERROR\"))\r\n F n = If (n <=? 8) Int DUMMY\r\n\r\ntest :: (F n ~ Word) => Proxy n -> Int\r\ntest _ = 2\r\n\r\ntest2 :: Proxy (n :: Nat) -> Int\r\ntest2 p = test p\r\n\r\nmain :: IO ()\r\nmain = do\r\n print (test2 (Proxy :: Proxy 5))\r\n}}}\r\n\r\nThe type error is useful:\r\n{{{\r\nBug.hs:26:11: error:\r\n • Couldn't match type ‘If (n <=? 8) Int DUMMY’ with ‘Word’\r\n arising from a use of ‘test’\r\n • In the expression: test p\r\n In an equation for ‘test2’: test2 p = test p\r\n • Relevant bindings include\r\n p :: Proxy n (bound at Bug.hs:26:7)\r\n test2 :: Proxy n -> Int (bound at Bug.hs:26:1)\r\n |\r\n26 | test2 p = test p\r\n | ^^^^^^\r\n}}}\r\n\r\nNow if we use the commented implementation of `F` (using `TypeError`), with GHC 8.2.2 and 8.0.2 we get:\r\n{{{\r\nBug.hs:26:11: error:\r\n • ERROR\r\n • In the expression: test p\r\n In an equation for ‘test2’: test2 p = test p\r\n |\r\n26 | test2 p = test p\r\n | ^^^^^^\r\n}}}\r\n\r\nWhile with GHC 8.0.1 we get:\r\n{{{\r\n/home/hsyl20/tmp/Bug.hs:29:11: error:\r\n • Couldn't match type ‘If (n <=? 8) Int (TypeError ...)’\r\n with ‘Word’\r\n arising from a use of ‘test’\r\n • In the expression: test p\r\n In an equation for ‘test2’: test2 p = test p\r\n}}}\r\n\r\n1) Could we restore the behavior of GHC 8.0.1?\r\n\r\n2) In my real code, when I use DUMMY I get:\r\n{{{\r\n • Couldn't match type ‘If (n <=? 8) Int8 DUMMY’ with ‘Word’\r\n Expected type: Word\r\n Actual type: F n\r\n}}}\r\nIf we could get the same report (mentioning the \"Actual type\") when we use `TypeError` that would be great.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13775Type family expansion is too lazy, allows accepting of ill-typed terms2021-12-17T15:02:30ZfizrukType family expansion is too lazy, allows accepting of ill-typed termsI'm using GHC 8.0.2 and I've just witnessed a weird bug.
To reproduce a bug I use this type family, using `TypeError` (this is a minimal type family I could get to keep bug reproducible):
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE Typ...I'm using GHC 8.0.2 and I've just witnessed a weird bug.
To reproduce a bug I use this type family, using `TypeError` (this is a minimal type family I could get to keep bug reproducible):
```
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits
type family Head xs where
Head '[] = TypeError (Text "empty list")
Head (x ': xs) = x
```
Then I go to GHCi, load this code and observe this:
```
>>> show (Proxy @ (Head '[]))
"Proxy"
```
This looks like a bug to me! I expect `Head '[]` to produce a type error.
And indeed it does, if I ask differently:
```
>>> Proxy @ (Head '[])
<interactive>:9:1: error:
• empty list
• When checking the inferred type
it :: Proxy (TypeError ...)
```
So far it looks like `show` somehow "lazily" evaluates it's argument type and that's why it's possible to `show Proxy` even when `Proxy` is ill-typed.
But if I expand `Head '[]` manually then it all works as expected again:
```
>>> show $ Proxy @ (TypeError (Text "error"))
<interactive>:13:8: error:
• error
• In the second argument of ‘($)’, namely
‘Proxy @(TypeError (Text "error"))’
In the expression: show $ Proxy @(TypeError (Text "error"))
In an equation for ‘it’:
it = show $ Proxy @(TypeError (Text "error"))
```
You can remove `TypeError` from the original type family:
```
type family Head xs where
Head (x ': xs) = x
```
And it gets even weirder:
```
>>> show (Proxy @ (Head '[]))
"Proxy"
>>> Proxy @ (Head '[])
Proxy
```
I did not test this with GHC 8.2.
I think this behaviour is not critical for me, but accepting ill-typed terms looks like a bad sign, especially for type-level-heavy programs.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | MacOS X |
| Architecture | x86_64 (amd64) |
</details>
<!-- {"blocked_by":[],"summary":"Type family expansion is too lazy, allows accepting of ill-typed terms","status":"New","operating_system":"MacOS X","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"x86_64 (amd64)","cc":[""],"type":"Bug","description":"I'm using GHC 8.0.2 and I've just witnessed a weird bug.\r\n\r\nTo reproduce a bug I use this type family, using `TypeError` (this is a minimal type family I could get to keep bug reproducible):\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\n\r\nimport GHC.TypeLits\r\n\r\ntype family Head xs where\r\n Head '[] = TypeError (Text \"empty list\")\r\n Head (x ': xs) = x\r\n}}}\r\n\r\nThen I go to GHCi, load this code and observe this:\r\n\r\n{{{\r\n>>> show (Proxy @ (Head '[]))\r\n\"Proxy\"\r\n}}}\r\n\r\nThis looks like a bug to me! I expect `Head '[]` to produce a type error.\r\nAnd indeed it does, if I ask differently:\r\n\r\n{{{\r\n>>> Proxy @ (Head '[])\r\n\r\n<interactive>:9:1: error:\r\n • empty list\r\n • When checking the inferred type\r\n it :: Proxy (TypeError ...)\r\n}}}\r\n\r\nSo far it looks like `show` somehow \"lazily\" evaluates it's argument type and that's why it's possible to `show Proxy` even when `Proxy` is ill-typed.\r\n\r\nBut if I expand `Head '[]` manually then it all works as expected again:\r\n\r\n{{{\r\n>>> show $ Proxy @ (TypeError (Text \"error\"))\r\n\r\n<interactive>:13:8: error:\r\n • error\r\n • In the second argument of ‘($)’, namely\r\n ‘Proxy @(TypeError (Text \"error\"))’\r\n In the expression: show $ Proxy @(TypeError (Text \"error\"))\r\n In an equation for ‘it’:\r\n it = show $ Proxy @(TypeError (Text \"error\"))\r\n}}}\r\n\r\nYou can remove `TypeError` from the original type family:\r\n\r\n{{{\r\ntype family Head xs where\r\n Head (x ': xs) = x\r\n}}}\r\n\r\nAnd it gets even weirder:\r\n\r\n{{{\r\n>>> show (Proxy @ (Head '[]))\r\n\"Proxy\"\r\n>>> Proxy @ (Head '[])\r\nProxy\r\n}}}\r\n\r\nI did not test this with GHC 8.2.\r\n\r\nI think this behaviour is not critical for me, but accepting ill-typed terms looks like a bad sign, especially for type-level-heavy programs.","type_of_failure":"OtherFailure","blocking":[]} -->Iavor S. DiatchkiIavor S. Diatchkihttps://gitlab.haskell.org/ghc/ghc/-/issues/12049`OverloadedStrings` for types2019-07-07T18:27:51ZIcelandjack`OverloadedStrings` for typesIs there any sense in adding
```hs
class IsSymbol a where
type FromSymbol (str :: Symbol) :: a
instance IsSymbol ErrorMessage where
type FromSymbol str = GHC.TypeLits.Text str
instance IsSymbol ErrorMessage where
type FromSymbol...Is there any sense in adding
```hs
class IsSymbol a where
type FromSymbol (str :: Symbol) :: a
instance IsSymbol ErrorMessage where
type FromSymbol str = GHC.TypeLits.Text str
instance IsSymbol ErrorMessage where
type FromSymbol str = str
```
where `FromSymbol` gets placed before type-level string literals:
```hs
TypeError ("Warning: ":<>:ShowType ty:<>:" is odd.")
```
analogous to `Data.String.IsString`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.10.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"`OverloadedStrings` for types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":["CustomTypeErrors"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Is there any sense in adding\r\n\r\n{{{#!hs\r\nclass IsSymbol a where\r\n type FromSymbol (str :: Symbol) :: a\r\n\r\ninstance IsSymbol ErrorMessage where\r\n type FromSymbol str = GHC.TypeLits.Text str\r\n\r\ninstance IsSymbol ErrorMessage where\r\n type FromSymbol str = str\r\n}}}\r\n\r\nwhere `FromSymbol` gets placed before type-level string literals:\r\n\r\n{{{#!hs\r\nTypeError (\"Warning: \":<>:ShowType ty:<>:\" is odd.\")\r\n}}}\r\n\r\nanalogous to `Data.String.IsString`.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12048Allow CustomTypeErrors in type synonyms (+ evaluate nested type family?)2021-08-14T20:16:35ZIcelandjackAllow CustomTypeErrors in type synonyms (+ evaluate nested type family?)I didn't find a ticket with this, but with wiki:Proposal/CustomTypeErrors you can't define a type synonym without it erroring:
```hs
-- error: …
-- • onetwothree
-- • In the type synonym declaration for ‘ERROR’
-- Compilation fa...I didn't find a ticket with this, but with wiki:Proposal/CustomTypeErrors you can't define a type synonym without it erroring:
```hs
-- error: …
-- • onetwothree
-- • In the type synonym declaration for ‘ERROR’
-- Compilation failed.
type ERROR = TypeError (Text "onetwothree")
```
but I often want to factor out error messages, they are clunky to write at the type level and I often want to reuse message in many different type families, especially when they can be determined by a type family. Here's a hypothetical example:
```hs
type family
Whoami (ty :: Type) :: Symbol where
Whoami Int = "a number"
Whoami Float = "a number"
Whoami [_] = "a list of things"
Whoami _ = "something else"
```
I would like to write
```hs
type Error ty =
TypeError (Text "Expected a <...> but got ":<>: Text (Whoami ty))
```
----
Even when ‘inlined’, it displays `Expected a GRUE but got 'Text (Whoami Int)` and not `• Expected a GRUE but got a number.`:
```hs
a :: TypeError (Text "Expected a GRUE but got ":<>: Text (Whoami Int))
a = 'a'
```Iavor S. DiatchkiIavor S. Diatchkihttps://gitlab.haskell.org/ghc/ghc/-/issues/11967Custom message when showing functions, comparing functions, ...2024-02-22T01:14:49ZIcelandjackCustom message when showing functions, comparing functions, ...One of the [examples](https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomTypeErrors#Examples) of type errors:
```hs
instance TypeError (Text "Cannot 'Show' functions." :$$:
Text "Perhaps there is a missing argumen...One of the [examples](https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomTypeErrors#Examples) of type errors:
```hs
instance TypeError (Text "Cannot 'Show' functions." :$$:
Text "Perhaps there is a missing argument?")
=> Show (a -> b) where
showsPrec = error "unreachable"
```
We already have [Text.Show.Functions](https://hackage.haskell.org/package/base-4.8.2.0/docs/src/Text.Show.Functions.html), is there a place in `base` for this along with `Ord (a -> b)` instances and co.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.10.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Custom message when showing functions, comparing functions, ...","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"One of the [https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomTypeErrors#Examples examples] of type errors:\r\n\r\n{{{#!hs\r\ninstance TypeError (Text \"Cannot 'Show' functions.\" :$$: \r\n Text \"Perhaps there is a missing argument?\")\r\n => Show (a -> b) where\r\n showsPrec = error \"unreachable\"\r\n}}}\r\n\r\nWe already have [https://hackage.haskell.org/package/base-4.8.2.0/docs/src/Text.Show.Functions.html Text.Show.Functions], is there a place in `base` for this along with `Ord (a -> b)` instances and co.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11581TypeError requires UndecidableInstances unnecessarily2021-08-03T22:02:50ZrwbartonTypeError requires UndecidableInstances unnecessarilyThe example from the `TypeError` documentation
```hs
type family ByteSize x where
ByteSize Word16 = 2
ByteSize Word8 = 1
ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
...The example from the `TypeError` documentation
```hs
type family ByteSize x where
ByteSize Word16 = 2
ByteSize Word8 = 1
ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
Text " is not exportable.")
```
requires `UndecidableInstances`:
```
BS.hs:11:5: error:
• The type family application ‘(TypeError ...)’
is no smaller than the instance head
(Use UndecidableInstances to permit this)
• In the equations for closed type family ‘ByteSize’
In the type family declaration for ‘ByteSize’
```
Obviously there's no real danger of undecidability here.
I tried changing the declaration of `TypeError` to
```hs
type family TypeError :: ErrorMessage -> b where
```
but it didn't help. Same error. Is that a bug?https://gitlab.haskell.org/ghc/ghc/-/issues/11099Incorrect warning about redundant constraints2019-07-07T18:32:07ZIavor S. DiatchkiIncorrect warning about redundant constraintsThe following program results in an incorrect warning about a redundant constraint:
```
{-# LANGUAGE TypeFamilies #-}
type family SomeFun a
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
f _ = read "HELLO"
```
This is the warning:
...The following program results in an incorrect warning about a redundant constraint:
```
{-# LANGUAGE TypeFamilies #-}
type family SomeFun a
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
f _ = read "HELLO"
```
This is the warning:
```
Redundant constraint: SomeFun i ~ [a]
In the type signature for:
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
```
I tried it on GHC version 7.11.20151029
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Incorrect warning about redundant constraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program results in an incorrect warning about a redundant constraint:\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\ntype family SomeFun a \r\n\r\nf :: (SomeFun i ~ [a], Read a) => proxy i -> a\r\nf _ = read \"HELLO\"\r\n}}}\r\n\r\nThis is the warning:\r\n{{{\r\nRedundant constraint: SomeFun i ~ [a]\r\n In the type signature for:\r\n f :: (SomeFun i ~ [a], Read a) => proxy i -> a\r\n}}}\r\n\r\nI tried it on GHC version 7.11.20151029\r\n","type_of_failure":"OtherFailure","blocking":[]} -->