GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-08-22T18:17:56Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/23816Instances with Unsatisfiable context should use unsatisfiable for missing met...2023-08-22T18:17:56Zsheafsam.derbyshire@gmail.comInstances with Unsatisfiable context should use unsatisfiable for missing methods even when they have defaultsCurrently, we only generate method implementations for instances with an `Unsatisfiable` context when they have no default implementation. However, this can cause problems, e.g.
```haskell
{-# OPTIONS_GHC -fdefer-type-errors #-}
module...Currently, we only generate method implementations for instances with an `Unsatisfiable` context when they have no default implementation. However, this can cause problems, e.g.
```haskell
{-# OPTIONS_GHC -fdefer-type-errors #-}
module T23816 where
instance Unsatisfiable (Text "Msg") => Eq (a -> b)
bad = id == id
```
calling `bad` will result in a runtime loop due to `(==)` having a default definition in terms of `(/=)` and vice-versa, when we would rather it throws the unsatisfiable type error.
The fix is to change `GHC.Tc.TyCl.Instance.tc_default` to always create an `unsatisfiable` RHS even when there is a default method. I will execute.9.8.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23128Incorrect `@since` annotations in `GHC.TypeError`2023-03-22T09:48:46ZBen PriceIncorrect `@since` annotations in `GHC.TypeError`## Summary
(I *think* that base-4.16 and GHC-9.2 are synonymous, as are base-4.17 and GHC-9.4, if not then this report may be incorrect)
Location of documentation issue: Haddocks of `base`, changelog of `base`
`GHC.TypeError` says `@s...## Summary
(I *think* that base-4.16 and GHC-9.2 are synonymous, as are base-4.17 and GHC-9.4, if not then this report may be incorrect)
Location of documentation issue: Haddocks of `base`, changelog of `base`
`GHC.TypeError` says `@since 4.16.0.0`
- in the module header (https://gitlab.haskell.org/ghc/ghc/-/blob/master/libraries/base/GHC/TypeError.hs#L15)
- on `type Assert` (https://gitlab.haskell.org/ghc/ghc/-/blob/master/libraries/base/GHC/TypeError.hs#L135)
Similarly, the changelog of base says, under "Documentation Fixes > 4.16.0.0"
> Comparison constraints in Data.Type.Ord (e.g. <=) now use the new GHC.TypeError.Assert type family instead of type equality with ~.
Note that the changelog of base says (correctly in the 4.17 section)
> Add GHC.TypeError module to contain functionality related to custom type errors. TypeError is re-exported from GHC.TypeLits for backwards compatibility.
Note these two changelog fragments are inconsistent wrt when this was introduced!
The PR that introduced the module and type was !6066, which only landed in GHC-9.4==base-4.17.0.0.
## Proposed improvements or changes
I think the correct thing is
- Change these to `@since 4.17.0.0`
- move the changelog entry upRodrigo MesquitaRodrigo Mesquitahttps://gitlab.haskell.org/ghc/ghc/-/issues/23076strange interaction of `deriving` and `TypeError` makes it so that `TypeError...2023-03-06T12:45:55ZMagnus Viernickelstrange interaction of `deriving` and `TypeError` makes it so that `TypeError`s get deferred to the useage sites## Summary
When trying to `anyclass` or `via` derive an instance that uses an instance that has a `TypeError` constraint, the `TypeError` doesn't where the instance is derived but rather where the instance is used; if the instance is wr...## Summary
When trying to `anyclass` or `via` derive an instance that uses an instance that has a `TypeError` constraint, the `TypeError` doesn't where the instance is derived but rather where the instance is used; if the instance is written manually, the error appears as expected.
## Steps to reproduce
- load this code and try to run `allFinite @A`, this will result in the expected type error, however, if you comment out the manually written instance at the bottom, this will immediately result in a type error.
<details><summary>the error</summary>
```
<interactive>:1:1: error:
• Bool in constr of type
• In the expression: allFinite @A
In an equation for ‘it’: it = allFinite @A
(0.00 secs,)
```
</details>
```haskell
class Finite a where
allFinite :: [a]
default allFinite :: (Generic a, GFinite (Rep a)) => [a]
allFinite = gallFinite
newtype Generically a = Generically a
deriving stock (Eq, Ord, Show, Generic)
instance (Generic a, GFinite (Rep a)) => Finite (Generically a) where
allFinite = coerce (gallFinite @a)
gallFinite :: forall a. (GFinite (Rep a), Generic a) => [a]
gallFinite = do
to <$> gfinite @(Rep a)
class GFinite f where
gfinite :: [f a]
instance
TypeError ('ShowType c ':<>: 'Text " in constr of type")
=> GFinite (K1 r c)
where
gfinite = error "someone removed the Type error constraint"
instance GFinite f => GFinite (M1 i t f) where
gfinite = M1 <$> gfinite
newtype A = MkA Bool
deriving stock (Generic, Show)
-- this should err
-- deriving (Finite) via (Generically A)
-- this should also err
deriving anyclass (Finite)
-- this errs as expected with "Bool in constr of type"
-- instance Finite A where
-- allFinite = gallFinite
```
I hope the reproducer is small enough...
## Expected behavior
I expect both of the deriving clauses to err instead of deferring the error to the usage site; especially the `anyclass` example I expect to behave identically to the manually written instance.
> **Note**
>
> I first thought that this was deferred to runtime due to my tests in GHCi, that's why I closed and reopened. Sorry for that
## Environment
* GHC version used: `925`, `944`
* Operating System: `NixOS 22.11`
* System Architecture: `x86_64-linux`https://gitlab.haskell.org/ghc/ghc/-/issues/22105Odd interation between ambiguity check, instance constraint, and fundeps2022-08-24T22:09:32ZDavid FeuerOdd interation between ambiguity check, instance constraint, and fundeps## Summary
I suspect this might be related to #21149, but it doesn't look quite the same so I figured I'd report it anyway. A custom type error is reported in a situation where it's not at all obvious why the `TypeError` in question is ...## Summary
I suspect this might be related to #21149, but it doesn't look quite the same so I figured I'd report it anyway. A custom type error is reported in a situation where it's not at all obvious why the `TypeError` in question is even being inspected.
## Steps to reproduce
```haskell
{-# language DataKinds, PolyKinds, FunctionalDependencies, AllowAmbiguousTypes, UndecidableInstances #-}
module AmbTE where
import GHC.TypeLits
import Data.Proxy
class xs ~ (hd ': tl) =>
HeadTail (msg :: ErrorMessage) (xs :: [k]) (hd :: k) (tl :: [k])
| xs -> hd tl, hd tl -> xs
instance xs ~ (hd ': tl) => HeadTail msg xs hd tl
instance {-# INCOHERENT #-}
(TypeError msg, '[] ~ (hd ': tl)) => HeadTail msg '[] hd tl
foo :: forall {k} (xs :: [k]) (hd :: k) (tl :: [k]). HeadTail ('Text "whoopsy") xs hd tl => Proxy '(hd, tl)
foo = Proxy
```
This reports
```haskell
AmbTE.hs:10:8: error:
• whoopsy
• In the ambiguity check for ‘foo’
In the type signature:
foo :: forall {k}
(xs :: [k])
(hd :: k)
(tl :: [k]). HeadTail ('Text "whoopsy") xs hd tl => Proxy '(hd, tl)
|
10 | foo :: forall {k} (xs :: [k]) (hd :: k) (tl :: [k]). HeadTail ('Text "whoopsy") xs hd tl => Proxy '(hd, tl)
```
Since I don't see any `'[]` in that type signature, it seems rather surprising to get the type error!
After writing the above, I realized that the fundeps are actually *redundant*. Removing them, surprisingly, makes it compile!
## Expected behavior
I'd expect the above to compile.
## Environment
* GHC version used: 9.4.1
Optional:
* Operating System:
* System Architecture:https://gitlab.haskell.org/ghc/ghc/-/issues/21149servant-0.19 fails to compile on HEAD due to TypeErrors triggering more eagerly2022-08-24T17:52:16ZRyan Scottservant-0.19 fails to compile on HEAD due to TypeErrors triggering more eagerly`servant-0.19` fails to build on GHC HEAD. Here is a minimized version of the issue:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE PolyKi...`servant-0.19` fails to build on GHC HEAD. Here is a minimized version of the issue:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
import GHC.TypeLits
-- | No instance exists for @tycls (expr :> ...)@ because
-- @expr@ is not recognised.
type NoInstanceForSub (tycls :: k) (expr :: k') =
Text "There is no instance for " :<>: ShowType tycls
:<>: Text " (" :<>: ShowType expr :<>: Text " :> ...)"
-- | No instance exists for @expr@.
type NoInstanceFor (expr :: k) =
Text "There is no instance for " :<>: ShowType expr
-- | No instance exists for @tycls (expr :> ...)@ because @expr@ is not fully saturated.
type PartialApplication (tycls :: k) (expr :: k') =
NoInstanceForSub tycls expr
:$$: ShowType expr :<>: Text " expects " :<>: ShowType (Arity expr) :<>: Text " more arguments"
-- The arity of a combinator, i.e. the number of required arguments.
type Arity (ty :: k) = Arity' k
type Arity' :: k -> Nat
type family Arity' (ty :: k) :: Nat where
Arity' (_ -> ty) = 1 + Arity' ty
Arity' _ = 0
data (path :: k) :> (a :: *)
class HasLink endpoint where
instance TypeError (PartialApplication HasLink arr) => HasLink ((arr :: a -> b) :> sub)
```
This compiles with GHC 9.0.2 and 9.2.1, but fails to compile with HEAD:
```
$ ~/Software/ghc-9.3.20220216/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:40:10: error:
• There is no instance for HasLink (arr :> ...)
arr expects 1 + Arity' b more arguments
• In the ambiguity check for an instance declaration
In the instance declaration for ‘HasLink ((arr :: a -> b) :> sub)’
|
40 | instance TypeError (PartialApplication HasLink arr) => HasLink ((arr :: a -> b) :> sub)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
I'm unclear if this change is intended behavior or not, but since I couldn't find any mention of `TypeError`'s behavior changing in the [9.4 release notes](https://gitlab.haskell.org/ghc/ghc/-/blob/d734ef8f78203b856dcfaf19eaebfed6ec623850/docs/users_guide/9.4.1-notes.rst), I decided to open an issue.9.4.1sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20835Implement Unsatisfiable as an alternative to TypeError2023-04-30T23:03:52ZAdam GundryImplement Unsatisfiable as an alternative to TypeErrorThis proposal has been accepted: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst
Implementing this will require extending `GHC.TypeError` with the following definitions, and adding special-pur...This proposal has been accepted: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0433-unsatisfiable.rst
Implementing this will require extending `GHC.TypeError` with the following definitions, and adding special-purpose behaviour to `Unsatisfiable` constraints as described in the proposal. This will provide an alternative to `TypeError` that is more clearly specified.
```hs
class Unsatisfiable (e :: ErrorMessage) where
unsatisfiableLifted :: a
unsatisfiable :: forall (e :: ErrorMessage) {rep} (a :: TYPE rep). Unsatisfiable e => a
unsatisfiable = unsatisfiableLifted @e @((# #) -> a) (# #)
```
Would anyone be interested in implementing this?sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/20241TypeError reporting is too aggressive2021-08-18T22:29:09ZSimon Peyton JonesTypeError reporting is too aggressiveSummary: we are reporting `TypeError` calls too aggressively. This is blocking !6066. An easy fix is available.
Consider this, [derived from an ongoing MR](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6066/diffs#note_371704).
`...Summary: we are reporting `TypeError` calls too aggressively. This is blocking !6066. An easy fix is available.
Consider this, [derived from an ongoing MR](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6066/diffs#note_371704).
```
type Assert :: Bool -> Constraint -> Constraint
type family Assert check errMsg where
Assert 'True _ = ()
Assert _ errMsg = errMsg
foo_sym :: Assert 'True (TypeError (Text "Boom")) => Proxy a -> ()
foo_sym Proxy = ()
```
We get
```
T6066.hs:14:12: error:
• Boom
• In the type signature:
foo_sym :: Assert 'True (TypeError (Text "Boom")) => Proxy a -> ()
|
14 | foo_sym :: Assert 'True (TypeError (Text "Boom")) => Proxy a -> ()
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But this is silly: the `Assert` call is going to discard that `TypeError`. And not only is it silly, it actually prevents some useful applications of `TypeError`. Here is a less contrived signature:
```
foo_sym :: forall a. (Assert (IsInt a) ErrSyn) => Proxy a -> ()
```
We want to blow up on *calls* of `foo_sym` where `IsInt a` turns out to be False.
You can hide the `TypeError` inside a nullary type family like this:
```
type family HiddenTypeError where
HiddenTypeError = TypeError (Text "Boom")
foo_sym :: Assert 'True HiddenTypeError => Proxy a -> ()
```
but that is obviously grotesque.
## Proposed solution
When checking the validity of a user-written type signature (in `GHC.Tc.Validity.checkValidType`), we currently complain if `TypeError` occurs anywhere. Proposed solution:
* `checkValidType` complains of `TypeError`, *ignoring occurrences in the argument of a type family*
So it would not look at the arguments of `Assert` above.
Any views? This is closely related to #20180 and #20181.https://gitlab.haskell.org/ghc/ghc/-/issues/20181TypeError should be ok in a synonym2021-08-17T11:51:29ZSimon Peyton JonesTypeError should be ok in a synonymIf you write
```
type Foo = TypeError (Text "foo")
```
you get the perplexing message
```
Foo.hs:21:1: error:
• foo
• In the type synonym declaration for ‘Foo’
|
21 | type Foo a = TypeError (Text "foo")
| ^^^^^^^^^^^^^^^^^^...If you write
```
type Foo = TypeError (Text "foo")
```
you get the perplexing message
```
Foo.hs:21:1: error:
• foo
• In the type synonym declaration for ‘Foo’
|
21 | type Foo a = TypeError (Text "foo")
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But there is nothing wrong here! We just wanted to abbreviate the `TypeError` call -- this becomes jolly useful when the message is long.
The error comes from the call to `checkUserTypeError` in `checkValidType`, which is applied to the RHS of type synonyms.
My conclusion: don't call `checkUserTypeError` on the RHS of type synonyms
------------------------------------
See #18310, #20180, #12048, !6066https://gitlab.haskell.org/ghc/ghc/-/issues/20180Pattern match checker should treat TypeError as unsatisfiable2021-08-17T11:51:29ZSimon Peyton JonesPattern match checker should treat TypeError as unsatisfiableConsider this code from !6066
```
type (<=?) :: Int -> Int -> Bool
type (<=) x y = Assert (x <=? y) (TypeError blah-blah)
type family Assert (check :: Bool) (errMsg :: Constraint) :: Constraint where
Assert 'True _errMsg = (...Consider this code from !6066
```
type (<=?) :: Int -> Int -> Bool
type (<=) x y = Assert (x <=? y) (TypeError blah-blah)
type family Assert (check :: Bool) (errMsg :: Constraint) :: Constraint where
Assert 'True _errMsg = ()
Assert _check errMsg = errMsg
```
and this use:
```
data List n t where
Nil :: List 0 t
(:-) :: t -> List n t -> List (n+1) t
head' :: (1 <= n) => List n t -> t
head' (x :- _) = x -- No need for a Nil case!
```
The pattern match checker will want to check that the Nil case is unreachable.
In the Nil case, the `(1 <= n)` constraint becomes `1 <= 0`, which simplifies
(via `Assert`) to `TypeError blah-blah`.
**And that `TypeError @Constraint blahblah` should be treated as unsatisfiable by the pattern match checker!**
NB: there is [some discussion here](https://gitlab.haskell.org/ghc/ghc/-/issues/18310#note_295410)
about having an explicit `Unsatisfiable` constraint, a more
principled cousin of `TypeError`.
Actually this all came up in #11503, five years ago. Let's nail it!Sebastian GrafSebastian Grafhttps://gitlab.haskell.org/ghc/ghc/-/issues/18310Way to scrutinize on unsatisfiable constraint2023-04-30T23:03:52ZOleg GrenrusWay to scrutinize on unsatisfiable constraintThis is motivated by `-fdefer-type-errors` use,
which is broken otherwise. But also to avoid using `error`,
when GHC knows something is unreachable.
The prologue is not big:
```haskell
{-# LANGUAGE GADTs, DataKinds, UndecidableInstance...This is motivated by `-fdefer-type-errors` use,
which is broken otherwise. But also to avoid using `error`,
when GHC knows something is unreachable.
The prologue is not big:
```haskell
{-# LANGUAGE GADTs, DataKinds, UndecidableInstances #-}
{-# OPTIONS -fdefer-type-errors #-}
import GHC.TypeLits
```
The non-sense `Int ~ Char` cases are also an example
of unsatisfiable constraints, but the `TypeError` variant
is actually something you run into in practice:
```haskell
class Bar a where
bar :: a
instance TypeError ('Text "No.") => Bar Int where
bar = 42
```
One use case of above is to forbid some instance from existing.
E.g. `instance TypeError ('Text "ZipList cannot be made into Monad") => Monad ZipList where ...`.
Yet, with a small indirection:
```haskell
*Main> let y = bar :: Int
<interactive>:10:9: warning: [-Wdeferred-type-errors]
• No.
• In the expression: bar :: Int
In an equation for ‘y’: y = bar :: Int
*Main> y
42
```
We do get a warning, but code still runs.
For that we need to somehow explicitly(?) scrutinize on impossible context,
or alternatively `TypeError`d instances should not require
any explicit implementations and implicit one created by GHC would throw the
(deferred) `TypeError`, not `No instance nor default method for class operation bar`.
It would be nicer to have some special expression constuct (in a spirit of `EmptyCase`),
to scrutinize dictionaries of impossible constraints.
I don't know what that syntax could look like.
So what I want is to be able to write
```haskell
instance TypeError ('Text "No.") => Bar Int where
```
which
1. won't give me a warning about unimplemented methods
2. with `-fdefer-type-errors` given methods will throw `TypeError`.
and a stretch goal is to have explicit syntax for these
"default" implementations too.
While I can replace implementations with `error "this shouldn't happen"`,
and then that error will be forced, we are not able to recover
an actual type-error in exception. That would be very useful for
testing `TypeError` machinery. Real use case: https://github.com/well-typed/optics/issues/322https://gitlab.haskell.org/ghc/ghc/-/issues/16906Custom type errors in default signatures are reported over-eagerly2023-04-30T23:03:52ZArtyom KazakCustom type errors in default signatures are reported over-eagerly# Summary
This piece of code triggers a custom type error:
```haskell
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
import GHC.TypeLits
class Foo a where
foo :: a
default foo ::...# Summary
This piece of code triggers a custom type error:
```haskell
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
import GHC.TypeLits
class Foo a where
foo :: a
default foo :: TypeError
(Text "Please define foo manually. Suggested definitions:" :$$:
Text " foo = something complicated" :$$:
Text " foo = something else complicated")
=> a
foo = error "unreachable"
```
```
default.hs:9:13-15: error: …
• Please define foo manually. Suggested definitions:
foo = something complicated
foo = something else complicated
• When checking the class method: foo :: forall a. Foo a => a
In the class declaration for ‘Foo’
|
```
# Expected behavior
I would expect the type error to be triggered on instance declarations, not the class declaration.
# Environment
* GHC version used: 8.6.5isovectorisovectorhttps://gitlab.haskell.org/ghc/ghc/-/issues/16377`TypeError` in a pattern should flag inaccessible code2021-08-15T13:19:00ZIavor S. Diatchki`TypeError` in a pattern should flag inaccessible codeWhen we pattern match, if the context ends up having a custom `TypeError`, we should probably report it, as we've essentially found some inaccessible code. At present this doesn't happen and the custom error is only triggered if the func...When we pattern match, if the context ends up having a custom `TypeError`, we should probably report it, as we've essentially found some inaccessible code. At present this doesn't happen and the custom error is only triggered if the function is applied to an invalid argument. Here is an example to illustrate the issue:
```
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GADTs #-}
module Test where
import GHC.TypeLits
import Data.Kind(Constraint)
type family F a :: Constraint
type instance F Int = ()
type instance F Char = TypeError ('Text "Nope")
type instance F Bool = (Int ~ Char)
data T where
A :: F Int => T
B :: F Char => T
C :: F Bool => T
exhaustive :: T -> ()
exhaustive A = ()
exhaustive B = () -- this is not flagged as inaccessible, but it should
-- exhaustive C = () -- this is flagged as inaccessible, as expected
```
If the match with constructor `C` is added to the program, GHC detects that this equation is inaccessible because `Int` will never match `Char`. I think that we'd like the same to happen in the second equation when we match on `B`, except we should report the custom type error, instead of GHC's message about unreachable code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.6.3 |
| 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` in a pattern should flag inaccessible code","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When we pattern match, if the context ends up having a custom `TypeError`, we should probably report it, as we've essentially found some inaccessible code. At present this doesn't happen and the custom error is only triggered if the function is applied to an invalid argument. Here is an example to illustrate the issue:\r\n\r\n{{{\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\n{-# LANGUAGE GADTs #-}\r\n\r\nmodule Test where\r\n\r\nimport GHC.TypeLits\r\nimport Data.Kind(Constraint)\r\n\r\ntype family F a :: Constraint\r\ntype instance F Int = ()\r\ntype instance F Char = TypeError ('Text \"Nope\")\r\ntype instance F Bool = (Int ~ Char)\r\n\r\ndata T where\r\n A :: F Int => T\r\n B :: F Char => T\r\n C :: F Bool => T\r\n\r\nexhaustive :: T -> ()\r\nexhaustive A = ()\r\nexhaustive B = () -- this is not flagged as inaccessible, but it should\r\n-- exhaustive C = () -- this is flagged as inaccessible, as expected\r\n}}}\r\n\r\n\r\nIf the match with constructor `C` is added to the program, GHC detects that this equation is inaccessible because `Int` will never match `Char`. I think that we'd like the same to happen in the second equation when we match on `B`, except we should report the custom type error, instead of GHC's message about unreachable code.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16362Deriving a class via an instance that has a TypeError constraint using standa...2019-07-07T18:00:22Zj9794Deriving a class via an instance that has a TypeError constraint using standalone deriving fails during compilation.This bug occurs if I define an instance for a typeclass adding a TypeError constraint on the instance, and then I try to derive that instance using Deriving Via in combination with StandaloneDeriving.
This is the shortest example I was a...This bug occurs if I define an instance for a typeclass adding a TypeError constraint on the instance, and then I try to derive that instance using Deriving Via in combination with StandaloneDeriving.
This is the shortest example I was able to come up with:
```
{-# Language DataKinds, UndecidableInstances, StandaloneDeriving, DerivingVia #-}
import GHC.TypeLits
newtype NotNum a = NotNum a
instance (TypeError (Text "Not a num")) => Num (NotNum a) where
data Foo = Foo
deriving via (NotNum Foo) instance Num Foo
```
In this case, it'll fail in compilation with 'Not a Num'.
This only seems to happen when combining deriving via with standalone deriving, because if I derive the class like:
```
data Foo = Foo deriving Num via (NotNum Foo)
```
It works as expected (doesn't fail with my custom error until I actually try to use a Foo where I should use a Num)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Deriving a class via an instance that has a TypeError constraint using standalone deriving fails during compilation.","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This bug occurs if I define an instance for a typeclass adding a TypeError constraint on the instance, and then I try to derive that instance using Deriving Via in combination with StandaloneDeriving.\r\nThis is the shortest example I was able to come up with:\r\n\r\n{{{\r\n{-# Language DataKinds, UndecidableInstances, StandaloneDeriving, DerivingVia #-} \r\n\r\nimport GHC.TypeLits\r\n\r\nnewtype NotNum a = NotNum a\r\n\r\ninstance (TypeError (Text \"Not a num\")) => Num (NotNum a) where\r\n\r\ndata Foo = Foo\r\nderiving via (NotNum Foo) instance Num Foo\r\n}}}\r\n\r\nIn this case, it'll fail in compilation with 'Not a Num'.\r\n\r\nThis only seems to happen when combining deriving via with standalone deriving, because if I derive the class like:\r\n\r\n{{{\r\ndata Foo = Foo deriving Num via (NotNum Foo)\r\n}}}\r\n\r\nIt works as expected (doesn't fail with my custom error until I actually try to use a Foo where I should use a Num)","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/16249no runtime error for -fdefer-type-errors with TypeError constraint2023-04-30T23:03:51ZGuillaume Bouchardno runtime error for -fdefer-type-errors with TypeError constraintPart of a testsuite, I'm using `-fdefer-type-errors` to check if haskell expression raises type error. However the haskell expression may be perfectly valid except for a `TypeError` constraint on a typeclass.
The following code:
```has...Part of a testsuite, I'm using `-fdefer-type-errors` to check if haskell expression raises type error. However the haskell expression may be perfectly valid except for a `TypeError` constraint on a typeclass.
The following code:
```haskell
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
import GHC.TypeLits
class Foo t where
foo :: t -> t
foo = id
instance Foo Int
instance (TypeError (Text "String does not work")) => Foo String
main :: IO ()
main = do
putStrLn (show (foo 10 :: Int))
putStrLn (foo "hello")
```
Correctly generates errors when compiled:
```
$ ghc ./DeferTypes.hs
[1 of 1] Compiling Main ( DeferTypes.hs, DeferTypes.o ) [flags changed]
DeferTypes.hs:17:13: error:
• String does not work
• In the first argument of ‘putStrLn’, namely ‘(foo "hello")’
In a stmt of a 'do' block: putStrLn (foo "hello")
In the expression:
do putStrLn (show (foo 10 :: Int))
putStrLn (foo "hello")
|
17 | putStrLn (foo "hello")
|
```
And also with `-fdefer-type-erros`, the error is transformed into a warning:
```
$ ghc -fdefer-type-errors ./DeferTypes.hs
[1 of 1] Compiling Main ( DeferTypes.hs, DeferTypes.o ) [flags changed]
DeferTypes.hs:17:13: warning: [-Wdeferred-type-errors]
• String does not work
• In the first argument of ‘putStrLn’, namely ‘(foo "hello")’
In a stmt of a 'do' block: putStrLn (foo "hello")
In the expression:
do putStrLn (show (foo 10 :: Int))
putStrLn (foo "hello")
|
17 | putStrLn (foo "hello")
| ^^^^^^^^^^^
Linking DeferTypes ...
```
However, executing the program gives no runtime error:
```
$ ./DeferTypes
10
hello
```
I was expecting something such as:
```
$ ./DeferTypes
10
[a defered type error exception]
```
With ghc 8.6.3 from nix.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"no runtime error for -fdefer-type-errors with TypeError constraint","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Part of a testsuite, I'm using `-fdefer-type-errors` to check if haskell expression raises type error. However the haskell expression may be perfectly valid except for a `TypeError` constraint on a typeclass.\r\n\r\nThe following code:\r\n\r\n{{{#!haskell\r\n{-# LANGUAGE UndecidableInstances #-}\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE DataKinds #-}\r\n\r\nimport GHC.TypeLits\r\n\r\nclass Foo t where\r\n foo :: t -> t\r\n foo = id\r\n\r\ninstance Foo Int\r\ninstance (TypeError (Text \"String does not work\")) => Foo String\r\n\r\nmain :: IO ()\r\nmain = do\r\n putStrLn (show (foo 10 :: Int))\r\n putStrLn (foo \"hello\")\r\n}}}\r\n\r\nCorrectly generates errors when compiled:\r\n\r\n{{{\r\n$ ghc ./DeferTypes.hs\r\n[1 of 1] Compiling Main ( DeferTypes.hs, DeferTypes.o ) [flags changed]\r\n\r\nDeferTypes.hs:17:13: error:\r\n • String does not work\r\n • In the first argument of ‘putStrLn’, namely ‘(foo \"hello\")’\r\n In a stmt of a 'do' block: putStrLn (foo \"hello\")\r\n In the expression:\r\n do putStrLn (show (foo 10 :: Int))\r\n putStrLn (foo \"hello\")\r\n |\r\n17 | putStrLn (foo \"hello\")\r\n | \r\n}}}\r\n\r\nAnd also with `-fdefer-type-erros`, the error is transformed into a warning:\r\n\r\n{{{\r\n$ ghc -fdefer-type-errors ./DeferTypes.hs\r\n[1 of 1] Compiling Main ( DeferTypes.hs, DeferTypes.o ) [flags changed]\r\n\r\nDeferTypes.hs:17:13: warning: [-Wdeferred-type-errors]\r\n • String does not work\r\n • In the first argument of ‘putStrLn’, namely ‘(foo \"hello\")’\r\n In a stmt of a 'do' block: putStrLn (foo \"hello\")\r\n In the expression:\r\n do putStrLn (show (foo 10 :: Int))\r\n putStrLn (foo \"hello\")\r\n |\r\n17 | putStrLn (foo \"hello\")\r\n | ^^^^^^^^^^^\r\nLinking DeferTypes ...\r\n}}}\r\n\r\nHowever, executing the program gives no runtime error:\r\n{{{\r\n$ ./DeferTypes \r\n10\r\nhello\r\n}}}\r\n\r\nI was expecting something such as:\r\n\r\n{{{\r\n$ ./DeferTypes\r\n10\r\n[a defered type error exception]\r\n}}}\r\n\r\nWith ghc 8.6.3 from nix.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15232TypeError is reported as "redundant constraint" starting with GHC 8.22019-07-07T18:13:41ZfsoikinTypeError is reported as "redundant constraint" starting with GHC 8.2The following program compiles fine on GHC 8.0.2, but GHC 8.2.2 issues a warning, complaining that `TypeError` is a redundant constraint. This makes it very inconvenient to use `TypeError` with type classes.
```hs
{-# OPTIONS_GHC -Wredu...The following program compiles fine on GHC 8.0.2, but GHC 8.2.2 issues a warning, complaining that `TypeError` is a redundant constraint. This makes it very inconvenient to use `TypeError` with type classes.
```hs
{-# OPTIONS_GHC -Wredundant-constraints -Wall -Werror #-}
import GHC.TypeLits (TypeError, ErrorMessage(..))
class C a where f :: a -> a
instance {-# OVERLAPPING #-} C Int where f _ = 42
instance {-# OVERLAPPABLE #-} TypeError ( 'Text "Only Int is supported" ) => C a where f = undefined
main :: IO ()
main = print $ f (42::Int)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeError is reported as \"redundant constraint\" starting with GHC 8.2","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["CustomTypeErrors"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program compiles fine on GHC 8.0.2, but GHC 8.2.2 issues a warning, complaining that `TypeError` is a redundant constraint. This makes it very inconvenient to use `TypeError` with type classes.\r\n\r\n{{{#!hs\r\n{-# OPTIONS_GHC -Wredundant-constraints -Wall -Werror #-}\r\nimport GHC.TypeLits (TypeError, ErrorMessage(..))\r\n\r\nclass C a where f :: a -> a\r\ninstance {-# OVERLAPPING #-} C Int where f _ = 42\r\ninstance {-# OVERLAPPABLE #-} TypeError ( 'Text \"Only Int is supported\" ) => C a where f = undefined\r\n\r\nmain :: IO ()\r\nmain = print $ f (42::Int)\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15052DeriveAnyClass instances may skip TypeError constraints2019-07-07T18:14:32ZDaniel GorínDeriveAnyClass instances may skip TypeError constraintsIn the presence of `TypeError`, one can derive instances with `DeriveAnyClass` that would be rejected otherwise. A simplistic example would be:
```haskell
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DataKinds #-}
{-# L...In the presence of `TypeError`, one can derive instances with `DeriveAnyClass` that would be rejected otherwise. A simplistic example would be:
```haskell
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module T
where
import GHC.TypeLits(TypeError, ErrorMessage(..))
class TypeError ('Text "BOOM") => C a where
f :: a -> ()
f _ = ()
data T = T
deriving(C)
```
Of course, any attempt to use the instance leads to a type-error. However, the instance is rejected right away using a normal instance declaration or StandaloneDeriving.
While this is a toy example, it can actually happen when using `Generics` and default-signatures, where one would puts a `TypeError` in an instance head for one of the `Generics` constructors to give a better error message.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"DeriveAnyClass instances may skip TypeError constraints","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In the presence of `TypeError`, one can derive instances with `DeriveAnyClass` that would be rejected otherwise. A simplistic example would be:\r\n\r\n{{{#!haskell\r\n{-# LANGUAGE DeriveAnyClass #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\n{-# LANGUAGE UndecidableSuperClasses #-}\r\nmodule T\r\n\r\nwhere\r\n\r\nimport GHC.TypeLits(TypeError, ErrorMessage(..))\r\n\r\n\r\nclass TypeError ('Text \"BOOM\") => C a where\r\n f :: a -> ()\r\n f _ = ()\r\n\r\n\r\ndata T = T\r\n deriving(C)\r\n\r\n}}}\r\n\r\nOf course, any attempt to use the instance leads to a type-error. However, the instance is rejected right away using a normal instance declaration or StandaloneDeriving.\r\n\r\nWhile this is a toy example, it can actually happen when using `Generics` and default-signatures, where one would puts a `TypeError` in an instance head for one of the `Generics` constructors to give a better error message.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14983Have custom type errors imply Void2023-04-30T23:03:51ZIcelandjackHave custom type errors imply VoidThis is a very minor issue, but `TypeError` (CustomTypeErrors) should entail a constraint like
```hs
import Data.Void
class (forall x. x) => No where
no :: Void
```
so users don't have to use `undefined` or `error ..`:
```hs
instan...This is a very minor issue, but `TypeError` (CustomTypeErrors) should entail a constraint like
```hs
import Data.Void
class (forall x. x) => No where
no :: Void
```
so users don't have to use `undefined` or `error ..`:
```hs
instance TypeError (Text "Can't show functions") => Show (a -> b) where
show :: (a -> b) -> String
show = no & absurd
```https://gitlab.haskell.org/ghc/ghc/-/issues/14339GHC 8.2.1 regression when combining GND with TypeError (solveDerivEqns: proba...2023-01-03T20:56:12ZRyan ScottGHC 8.2.1 regression when combining GND with TypeError (solveDerivEqns: probable loop)This code panics on GHC 8.2.1 and later:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import GHC.TypeLits
newtype Baz = Baz Foo
deriving Bar
new...This code panics on GHC 8.2.1 and later:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import GHC.TypeLits
newtype Baz = Baz Foo
deriving Bar
newtype Foo = Foo Int
class Bar a where
bar :: a
instance (TypeError (Text "Boo")) => Bar Foo where
bar = undefined
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64-unknown-linux):
solveDerivEqns: probable loop
DerivSpec
ds_loc = Bug.hs:9:12-14
ds_name = $fBarBaz
ds_tvs = []
ds_cls = Bar
ds_tys = [Baz]
ds_theta = [ThetaOrigin
to_tvs = []
to_givens = []
to_wanted_origins = [Bar Foo, (Foo :: *) ~R# (Baz :: *)]]
ds_mechanism = newtype
[[s0_a1D7[fuv:0]]]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcDerivInfer.hs:515:9 in ghc:TcDerivInfer
```
This is a regression since GHC 8.0.2, in which it does compile successfully.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC 8.2.1 regression when combining GND with TypeError (solveDerivEqns: probable loop)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["CustomTypeErrors","deriving,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code panics on GHC 8.2.1 and later:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE GeneralizedNewtypeDeriving #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport GHC.TypeLits\r\n\r\nnewtype Baz = Baz Foo\r\n deriving Bar\r\n\r\nnewtype Foo = Foo Int\r\n\r\nclass Bar a where\r\n bar :: a\r\n\r\ninstance (TypeError (Text \"Boo\")) => Bar Foo where\r\n bar = undefined\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.1 for x86_64-unknown-linux):\r\n solveDerivEqns: probable loop\r\n DerivSpec\r\n ds_loc = Bug.hs:9:12-14\r\n ds_name = $fBarBaz\r\n ds_tvs = []\r\n ds_cls = Bar\r\n ds_tys = [Baz]\r\n ds_theta = [ThetaOrigin\r\n to_tvs = []\r\n to_givens = []\r\n to_wanted_origins = [Bar Foo, (Foo :: *) ~R# (Baz :: *)]]\r\n ds_mechanism = newtype\r\n [[s0_a1D7[fuv:0]]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcDerivInfer.hs:515:9 in ghc:TcDerivInfer\r\n}}}\r\n\r\nThis is a regression since GHC 8.0.2, in which it does compile successfully.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/14141Custom type errors don't trigger when matching on a GADT constructor with an ...2021-08-15T13:19:00ZDarwin226Custom type errors don't trigger when matching on a GADT constructor with an error in the constraintThe following code fails to compile (as it should)
```hs
data D where
A :: C => D
type family C :: Constraint where
C = 'True ~ 'False
f :: D -> ()
f A = ()
```
with the error "Couldn't match type 'True with 'False".
This co...The following code fails to compile (as it should)
```hs
data D where
A :: C => D
type family C :: Constraint where
C = 'True ~ 'False
f :: D -> ()
f A = ()
```
with the error "Couldn't match type 'True with 'False".
This code, however, does compile without an issue:
```hs
data D where
A :: C => D
type family C :: Constraint where
C = TypeError ('Text "error")
f :: D -> ()
f A = ()
```
I feel that this is a bug.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | Windows |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Custom type errors don't trigger when matching on a GADT constructor with an error in the constraint","status":"New","operating_system":"Windows","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code fails to compile (as it should)\r\n\r\n{{{#!hs\r\ndata D where\r\n A :: C => D\r\n\r\ntype family C :: Constraint where\r\n C = 'True ~ 'False\r\n\r\nf :: D -> ()\r\nf A = ()\r\n}}}\r\n\r\nwith the error \"Couldn't match type 'True with 'False\".\r\n\r\nThis code, however, does compile without an issue:\r\n\r\n{{{#!hs\r\ndata D where\r\n A :: C => D\r\n\r\ntype family C :: Constraint where\r\n C = TypeError ('Text \"error\")\r\n\r\nf :: D -> ()\r\nf A = ()\r\n}}}\r\n\r\nI feel that this is a bug.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12237Constraint resolution vs. type family resolution vs. TypeErrors2019-07-07T18:27:01ZGergő ÉrdiConstraint resolution vs. type family resolution vs. TypeErrorsVia http://stackoverflow.com/q/37769351/477476, given the following setup:
```hs
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, UndecidableInstances #-}
import Data.Proxy
i...Via http://stackoverflow.com/q/37769351/477476, given the following setup:
```hs
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, UndecidableInstances #-}
import Data.Proxy
import GHC.TypeLits
type family TEq a b where
TEq a a = a
TEq a b = TypeError (Text "TEq error")
type family F a where
F () = ()
F (a, b) = TEq (F a) (F b)
F a = TypeError (Text "Unsupported type: " :<>: ShowType a)
```
and the following usages of `F` and `TEq`:
```hs
class (repr ~ F a) => C repr a
foo :: (C (F a) a) => proxy a -> ()
foo _ = ()
main :: IO ()
main = print $ foo (Proxy :: Proxy (Int, ()))
```
This results in
```
* No instance for (C (TEq (TypeError ...) ()) (Int, ()))
arising from a use of `foo'
* In the second argument of `($)', namely
`foo (Proxy :: Proxy (Int, ()))'
In the expression: print $ foo (Proxy :: Proxy (Int, ()))
In an equation for `main':
main = print $ foo (Proxy :: Proxy (Int, ()))
```
but it would be preferable to bail out earlier when `F Int` is resolved to `TypeError ...` instead of propagating that all the way to the `C` constraint.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.0.1 |
| 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":"Constraint resolution vs. type family resolution vs. TypeErrors","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["CustomTypeErrors"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Via http://stackoverflow.com/q/37769351/477476, given the following setup:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}\r\n{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, UndecidableInstances #-}\r\n\r\nimport Data.Proxy\r\nimport GHC.TypeLits\r\n\r\ntype family TEq a b where\r\n TEq a a = a\r\n TEq a b = TypeError (Text \"TEq error\")\r\n\r\ntype family F a where\r\n F () = ()\r\n F (a, b) = TEq (F a) (F b)\r\n F a = TypeError (Text \"Unsupported type: \" :<>: ShowType a)\r\n}}}\r\n\r\nand the following usages of `F` and `TEq`:\r\n\r\n{{{#!hs\r\nclass (repr ~ F a) => C repr a\r\n\r\nfoo :: (C (F a) a) => proxy a -> ()\r\nfoo _ = ()\r\n\r\nmain :: IO ()\r\nmain = print $ foo (Proxy :: Proxy (Int, ()))\r\n}}}\r\n\r\nThis results in\r\n\r\n{{{\r\n * No instance for (C (TEq (TypeError ...) ()) (Int, ()))\r\n arising from a use of `foo'\r\n * In the second argument of `($)', namely\r\n `foo (Proxy :: Proxy (Int, ()))'\r\n In the expression: print $ foo (Proxy :: Proxy (Int, ()))\r\n In an equation for `main':\r\n main = print $ foo (Proxy :: Proxy (Int, ()))\r\n}}}\r\n\r\nbut it would be preferable to bail out earlier when `F Int` is resolved to `TypeError ...` instead of propagating that all the way to the `C` constraint.","type_of_failure":"OtherFailure","blocking":[]} -->