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/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/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/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/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/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/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/12119Can't create injective type family equation with TypeError as the RHS2022-09-02T09:43:12ZRyan ScottCan't create injective type family equation with TypeError as the RHSFor the longest time, I've wanted to make a type family like this injective:
```hs
type family Foo (a :: *) :: * where
Foo Bar = Int
Foo Baz = Char
```
But the problem is that `Foo` is defined on //all// types of kind `*`, so the a...For the longest time, I've wanted to make a type family like this injective:
```hs
type family Foo (a :: *) :: * where
Foo Bar = Int
Foo Baz = Char
```
But the problem is that `Foo` is defined on //all// types of kind `*`, so the above definition is inherently non-injective. With the introduction of `TypeError`s, however, I thought I could rule out all other cases:
```hs
import GHC.TypeLits
type family Foo (a :: *) = (r :: *) | r -> a where
Foo Bar = Int
Foo Baz = Char
Foo _ = TypeError ('Text "boom")
```
But this doesn't work, sadly:
```
Injective.hs:18:3: error:
• Type family equations violate injectivity annotation:
Foo Bar = Int -- Defined at Injective.hs:18:3
Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
• In the equations for closed type family ‘Foo’
In the type family declaration for ‘Foo’
Injective.hs:20:3: error:
• Type family equation violates injectivity annotation.
Type variable ‘_’ cannot be inferred from the right-hand side.
In the type family equation:
Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
• In the equations for closed type family ‘Foo’
In the type family declaration for ‘Foo’
Injective.hs:20:3: error:
• Type family equation violates injectivity annotation.
RHS of injective type family equation cannot be a type family:
Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
• In the equations for closed type family ‘Foo’
In the type family declaration for ‘Foo’
```
From GHC's perspective, `TypeError` is just another type family, so it thinks it violates injectivity. But should this be the case? After all, having the RHS of a type family equation being `TypeError` is, in my perspective, tantamount to making that type family undefined for those inputs. It seems like if we successfully conclude that `Foo a ~ Foo b` (and GHC hasn't blown up yet due to type erroring), we should be able to conclude that `a ~ b`.
Could this be accomplished by simply adding a special case for `TypeError` in the injectivity checker?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire, jstolarek |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Can't create injective type family equation with TypeError as the RHS","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["CustomTypeErrors,","Injective","TypeFamilies,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","jstolarek"],"type":"FeatureRequest","description":"For the longest time, I've wanted to make a type family like this injective:\r\n\r\n{{{#!hs\r\ntype family Foo (a :: *) :: * where\r\n Foo Bar = Int\r\n Foo Baz = Char\r\n}}}\r\n\r\nBut the problem is that `Foo` is defined on //all// types of kind `*`, so the above definition is inherently non-injective. With the introduction of `TypeError`s, however, I thought I could rule out all other cases:\r\n\r\n{{{#!hs\r\nimport GHC.TypeLits\r\n\r\ntype family Foo (a :: *) = (r :: *) | r -> a where\r\n Foo Bar = Int\r\n Foo Baz = Char\r\n Foo _ = TypeError ('Text \"boom\")\r\n}}}\r\n\r\nBut this doesn't work, sadly:\r\n\r\n{{{\r\nInjective.hs:18:3: error: \r\n • Type family equations violate injectivity annotation: \r\n Foo Bar = Int -- Defined at Injective.hs:18:3 \r\n Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3\r\n • In the equations for closed type family ‘Foo’\r\n In the type family declaration for ‘Foo’\r\n\r\nInjective.hs:20:3: error:\r\n • Type family equation violates injectivity annotation.\r\n Type variable ‘_’ cannot be inferred from the right-hand side.\r\n In the type family equation:\r\n Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3\r\n • In the equations for closed type family ‘Foo’\r\n In the type family declaration for ‘Foo’\r\n\r\nInjective.hs:20:3: error:\r\n • Type family equation violates injectivity annotation.\r\n RHS of injective type family equation cannot be a type family:\r\n Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3\r\n • In the equations for closed type family ‘Foo’\r\n In the type family declaration for ‘Foo’\r\n}}}\r\n\r\nFrom GHC's perspective, `TypeError` is just another type family, so it thinks it violates injectivity. But should this be the case? After all, having the RHS of a type family equation being `TypeError` is, in my perspective, tantamount to making that type family undefined for those inputs. It seems like if we successfully conclude that `Foo a ~ Foo b` (and GHC hasn't blown up yet due to type erroring), we should be able to conclude that `a ~ b`.\r\n\r\nCould this be accomplished by simply adding a special case for `TypeError` in the injectivity checker?","type_of_failure":"OtherFailure","blocking":[]} -->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/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/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/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/11503TypeError woes (incl. pattern match checker)2021-08-15T13:19:00ZRichard Eisenbergrae@richarde.devTypeError woes (incl. pattern match checker)When I say
```
{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies,
UndecidableInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Bug where
import GHC.TypeLits
import GHC.Exts ( Constraint )
type...When I say
```
{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies,
UndecidableInstances #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Bug where
import GHC.TypeLits
import GHC.Exts ( Constraint )
type family NotInt a where
NotInt Int = TypeError (Text "That's Int, silly.")
NotInt _ = (() :: Constraint)
data T a where
MkT1 :: a -> T a
MkT2 :: NotInt a => T a
foo :: T Int -> Int
foo (MkT1 x) = x
```
I get
```
Bug.hs:19:1: warning:
Pattern match(es) are non-exhaustive
In an equation for ‘foo’: Patterns not matched: MkT2
```
But I shouldn't.
Even worse, perhaps, GHC accepts my pattern-match against `MkT2` if I add it. If I change the `TypeError` to `False ~ True`, I get the correct behavior.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.1 |
| 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 woes (incl. pattern match checker)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{\r\n{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies,\r\n UndecidableInstances #-}\r\n{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}\r\n\r\nmodule Bug where\r\n\r\nimport GHC.TypeLits\r\nimport GHC.Exts ( Constraint )\r\n\r\ntype family NotInt a where\r\n NotInt Int = TypeError (Text \"That's Int, silly.\")\r\n NotInt _ = (() :: Constraint)\r\n\r\ndata T a where\r\n MkT1 :: a -> T a\r\n MkT2 :: NotInt a => T a\r\n\r\nfoo :: T Int -> Int\r\nfoo (MkT1 x) = x\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nBug.hs:19:1: warning:\r\n Pattern match(es) are non-exhaustive\r\n In an equation for ‘foo’: Patterns not matched: MkT2\r\n}}}\r\n\r\nBut I shouldn't.\r\n\r\nEven worse, perhaps, GHC accepts my pattern-match against `MkT2` if I add it. If I change the `TypeError` to `False ~ True`, I get the correct behavior.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11391TypeError is fragile2019-07-07T18:30:37ZBen GamariTypeError is fragileConsider this use of the new `TypeError` feature,
```hs
{-# LANGUAGE TypeInType, TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind
import GHC.TypeLits (TypeError, ErrorMessage(..))
type fami...Consider this use of the new `TypeError` feature,
```hs
{-# LANGUAGE TypeInType, TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind
import GHC.TypeLits (TypeError, ErrorMessage(..))
type family Resolve (t :: Type -> Type) :: Type -> Type where
Resolve _ = TypeError (Text "ERROR")
```
#### The okay case
Given something like,
```hs
testOK :: Resolve [] Int
testOK = []
```
we find that things work as expected,
```
• ERROR
• In the expression: [] :: Resolve [] Int
In an equation for ‘testOK’: testOK = [] :: Resolve [] Int
```
#### The bad case
However, it is very easy to fool GHC into not yielding the desired error message. For instance,
```hs
testNOTOK1 :: Resolve [] Int
testNOTOK1 = ()
```
gives us this a unification error,
```
• Couldn't match type ‘()’ with ‘(TypeError ...)’
Expected type: Resolve [] Int
Actual type: ()
```
This clearly isn't what we expected.
#### The tricky case
Another way we can fool the typechecker is to make it attempt instance resolution on our `TypeError`,
```hs
testNOTOK2 :: Resolve [] Int
testNOTOK2 = 1
```
Which results in,
```
• No instance for (Num (TypeError ...))
arising from the literal ‘1’
• In the expression: 1
In an equation for ‘testNOTOK2’: testNOTOK2 = 1
```8.0.1Iavor S. DiatchkiIavor S. Diatchkihttps://gitlab.haskell.org/ghc/ghc/-/issues/12104Type families, `TypeError`, and `-fdefer-type-errors` cause "opt_univ fell in...2019-07-07T18:27:38ZantalszType families, `TypeError`, and `-fdefer-type-errors` cause "opt_univ fell into a hole"If I create a type family – open or closed – with a case that evaluates to a `TypeError`, and define a top-level binding with this type, loading the file with `-fdefer-type-errors` enabled (or via `:load!`/`:reload!`) panics GHC with "op...If I create a type family – open or closed – with a case that evaluates to a `TypeError`, and define a top-level binding with this type, loading the file with `-fdefer-type-errors` enabled (or via `:load!`/`:reload!`) panics GHC with "opt_univ fell into a hole". (And if I used `:load!` or `:reload!`, `-fdefer-type-errors` doesn't get unset.)
A minimal example:
```hs
{-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-}
module T12104 where
import GHC.TypeLits
type family F a where
F a = TypeError (Text "error")
err :: F ()
err = ()
```
results in the panic
```
….hs:9:7: warning: [-Wdeferred-type-errors]
• error
• In the expression: ()
In an equation for ‘err’: err = ()
ghc: panic! (the 'impossible' happened)
(GHC version 8.0.1 for x86_64-apple-darwin):
opt_univ fell into a hole {a4Va}
```
Adding more cases to the type family, or making it open, still cause the crash. This holds whether the error case is a final catch-all case, or something more like
```hs
type family F a where
F () = TypeError (Text "error")
F a = ()
```
Just using a type synonym for `F` doesn't cause a panic, however, and nor does giving `err` the type `TypeError (Text "error")` directly.8.2.1