GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2020-01-23T19:37:34Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11384Error says to fix incorrect return type2020-01-23T19:37:34ZIcelandjackError says to fix incorrect return typeDefining a constructor that returns the wrong type (non-parent type).
If the constructor is not fully-applied or over-saturated GHC reports an error, instead of telling the developer to change the return type:
```
Prelude> data A
Prelu...Defining a constructor that returns the wrong type (non-parent type).
If the constructor is not fully-applied or over-saturated GHC reports an error, instead of telling the developer to change the return type:
```
Prelude> data A
Prelude> data B a where MkB :: A ()
<interactive>:2:23: error:
• Expecting one fewer argument to ‘A’
Expected kind ‘* -> *’, but ‘A’ has kind ‘*’
• In the type ‘A ()’
In the definition of data constructor ‘MkB’
In the data declaration for ‘B’
```
Expected:
1. Suggest GADTs:
```
• Illegal generalised algebraic data declaration for ‘B’
(Use GADTs to allow GADTs)
• In the data declaration for ‘B’
```
1. Complain about incorrect return type:
```
• Data constructor ‘MkB’ returns type ‘A’
instead of an instance of its parent type ‘B a’
• In the definition of data constructor ‘MkB’
In the data type declaration for ‘B’
```
It shouldn't suggest the user fix the incorrect return type
<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":"Error says to fix incorrect return type","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["GADTs"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Defining a constructor that returns the wrong type (non-parent type).\r\n\r\nIf the constructor is not fully-applied or over-saturated GHC reports an error, instead of telling the developer to change the return type:\r\n\r\n{{{\r\nPrelude> data A\r\nPrelude> data B a where MkB :: A ()\r\n\r\n<interactive>:2:23: error:\r\n • Expecting one fewer argument to ‘A’\r\n Expected kind ‘* -> *’, but ‘A’ has kind ‘*’\r\n • In the type ‘A ()’\r\n In the definition of data constructor ‘MkB’\r\n In the data declaration for ‘B’\r\n}}}\r\n\r\nExpected:\r\n1. Suggest GADTs:\r\n{{{\r\n• Illegal generalised algebraic data declaration for ‘B’\r\n (Use GADTs to allow GADTs)\r\n• In the data declaration for ‘B’\r\n}}}\r\n2. Complain about incorrect return type:\r\n{{{\r\n• Data constructor ‘MkB’ returns type ‘A’ \r\n instead of an instance of its parent type ‘B a’\r\n• In the definition of data constructor ‘MkB’\r\n In the data type declaration for ‘B’\r\n}}}\r\n\r\nIt shouldn't suggest the user fix the incorrect return type","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11369Suppress redundant-constraint warnings in case of empty classes2020-01-23T19:37:34ZHerbert Valerio Riedelhvr@gnu.orgSuppress redundant-constraint warnings in case of empty classesThe technique described in
http://www.well-typed.com/blog/2015/07/checked-exceptions/
makes use of a class without any methods, i.e.
```hs
class Throws e
```
However, this by definition results in redundant constraints, e.g.
```hs
r...The technique described in
http://www.well-typed.com/blog/2015/07/checked-exceptions/
makes use of a class without any methods, i.e.
```hs
class Throws e
```
However, this by definition results in redundant constraints, e.g.
```hs
readFoo :: Throws IOError => FilePath -> IO Foo
readFoo fn = {- ... -}
```
which GHC 8.0 warns about.
I propose to suppress warnings in case a class which has no methods is used as seemingly redundant constraint.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | bgamari, edsko |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Suppress redundant-constraint warnings in case of empty classes","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.0.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"simonpj"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["bgamari","edsko"],"type":"Bug","description":"The technique described in\r\n\r\nhttp://www.well-typed.com/blog/2015/07/checked-exceptions/\r\n\r\nmakes use of a class without any methods, i.e.\r\n\r\n{{{#!hs\r\nclass Throws e\r\n}}}\r\n\r\nHowever, this by definition results in redundant constraints, e.g.\r\n\r\n{{{#!hs\r\nreadFoo :: Throws IOError => FilePath -> IO Foo\r\nreadFoo fn = {- ... -}\r\n}}}\r\n\r\nwhich GHC 8.0 warns about.\r\n\r\nI propose to suppress warnings in case a class which has no methods is used as seemingly redundant constraint.","type_of_failure":"OtherFailure","blocking":[]} -->Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/11352Allow applying type to label2023-06-05T11:55:16ZIcelandjackAllow applying type to label```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #...```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DataKinds #-}
import GHC.TypeLits
import GHC.OverloadedLabels
instance IsLabel "answer" Int where
fromLabel _ = 42
answer :: IsLabel "answer" a => a
answer = #answer
```
The follow works:
```hs
>>> answer @Int
42
```
but fails with a label:
```hs
>>> #answer @Int
<interactive>:...:1: error:
• Cannot not apply expression of type ‘t0’
to a visible type argument ‘Int’
• In the expression: #answer @Int
In an equation for ‘it’: it = #answer @Int
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.10.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Allow applying type to label","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"{{{#!hs\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE OverloadedLabels #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE DataKinds #-}\r\n\r\nimport GHC.TypeLits\r\nimport GHC.OverloadedLabels\r\n\r\ninstance IsLabel \"answer\" Int where\r\n fromLabel _ = 42\r\n\r\nanswer :: IsLabel \"answer\" a => a\r\nanswer = #answer\r\n}}}\r\n\r\nThe follow works:\r\n\r\n{{{#!hs\r\n>>> answer @Int\r\n42\r\n}}}\r\n\r\nbut fails with a label:\r\n\r\n{{{#!hs\r\n>>> #answer @Int\r\n<interactive>:...:1: error:\r\n • Cannot not apply expression of type ‘t0’\r\n to a visible type argument ‘Int’\r\n • In the expression: #answer @Int\r\n In an equation for ‘it’: it = #answer @Int\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->isovectorisovectorhttps://gitlab.haskell.org/ghc/ghc/-/issues/11186Give strong preference to type variable names in scope when reporting hole co...2019-07-07T18:31:35ZDavid FeuerGive strong preference to type variable names in scope when reporting hole contextsWhen using `ScopedTypeVariables` with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recentl...When using `ScopedTypeVariables` with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recently where that hasn't happened, but sometimes I've had a signature like
```hs
foo :: forall bar . ...
foo = ... _ ...
```
and yet the typed hole message shows that `bar` has been lost in unification and replaced by some unrelated name. I would very much prefer if this never happened.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| Type | FeatureRequest |
| 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":"Give strong preference to type variable names in scope when reporting hole contexts","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":["typed-holes"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"When using `ScopedTypeVariables` with typed holes, I want GHC to bend over backwards to preserve the names of type variables that the user has chosen to bring into scope. I can't immediately reproduce the situations I've run into recently where that hasn't happened, but sometimes I've had a signature like\r\n\r\n{{{#!hs\r\nfoo :: forall bar . ...\r\nfoo = ... _ ...\r\n}}}\r\n\r\nand yet the typed hole message shows that `bar` has been lost in unification and replaced by some unrelated name. I would very much prefer if this never happened.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11169Remove the word "skolem" from user error messages2019-07-07T18:31:39ZDavid FeuerRemove the word "skolem" from user error messagesSkolem variables are not, as best I can tell, part of the type system; they are part of the implementation of the type checking algorithm. As such, it seems inappropriate to mention them in error messages. Instead, the error messages sho...Skolem variables are not, as best I can tell, part of the type system; they are part of the implementation of the type checking algorithm. As such, it seems inappropriate to mention them in error messages. Instead, the error messages should explain things at the Haskell level.
```
Couldn't match expected type ‘t’ with actual type ‘a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by...
```
I'd much rather see an explanation using words like "existentially quantified" and "right-hand side of a pattern match".
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| Type | FeatureRequest |
| 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":"Remove the word \"skolem\" from user error messages","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Skolem variables are not, as best I can tell, part of the type system; they are part of the implementation of the type checking algorithm. As such, it seems inappropriate to mention them in error messages. Instead, the error messages should explain things at the Haskell level.\r\n\r\n{{{\r\n Couldn't match expected type ‘t’ with actual type ‘a’\r\n because type variable ‘a’ would escape its scope\r\n This (rigid, skolem) type variable is bound by...\r\n}}}\r\n\r\nI'd much rather see an explanation using words like \"existentially quantified\" and \"right-hand side of a pattern match\".","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11141Better error message when instance signature is incorrect2019-07-07T18:31:47ZEdward Z. YangBetter error message when instance signature is incorrectI was recently trying to solve an ambiguity error in a type class instance I was writing, and ended up with some code that looked like this (the ambiguity error has been eliminated for simplicity):
```
{-# LANGUAGE FunctionalDependencie...I was recently trying to solve an ambiguity error in a type class instance I was writing, and ended up with some code that looked like this (the ambiguity error has been eliminated for simplicity):
```
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
module A where
data F a = F a
instance Show a => Show (F a) where
show :: forall a. Show a => F a -> String
show (F x) = show x
```
This instance signature is incorrect: it's not necessary to add a universal quantifier to scope over type variables defined in the instance head; they are automatically in scope. But GHC unhelpfully reports:
```
ezyang@sabre:~$ Dev/ghc-7.10.2/usr/bin/ghci A.hs
GHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling A ( A.hs, interpreted )
A.hs:8:13:
Could not deduce (Show a0)
from the context (Show a)
bound by the type signature for show :: Show a => F a -> String
at A.hs:8:13-45
The type variable ‘a0’ is ambiguous
When checking that:
forall a. Show a => forall a1. Show a1 => F a1 -> String
is more polymorphic than: forall a. Show a => F a -> String
When checking that instance signature for ‘show’
is more general than its signature in the class
Instance sig: forall a.
Show a =>
forall a1. Show a1 => F a1 -> String
Class sig: forall a. Show a => F a -> String
In the instance declaration for ‘Show (F a)’
Failed, modules loaded: none.
```
Why did I get the wrong idea about how instance signatures work? Well, GHC doesn't warn if you write this:
```
instance Show a => Show (F a) where
show :: Show a => F a -> String
show (F x) = show x
```
Because this turns into a full type signature 'Show a, Show a =\> F a -\> String' (the first a and the second a end up getting unified.) I'm not sure if it should warn; it's an easy mistake to make if you are treating instance methods like plain function definitions (of course you have to write the full type signature...)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Better error message when instance signature is incorrect","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I was recently trying to solve an ambiguity error in a type class instance I was writing, and ended up with some code that looked like this (the ambiguity error has been eliminated for simplicity):\r\n\r\n{{{\r\n{-# LANGUAGE FunctionalDependencies #-}\r\n{-# LANGUAGE InstanceSigs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\nmodule A where\r\n\r\ndata F a = F a\r\ninstance Show a => Show (F a) where\r\n show :: forall a. Show a => F a -> String\r\n show (F x) = show x\r\n}}}\r\n\r\nThis instance signature is incorrect: it's not necessary to add a universal quantifier to scope over type variables defined in the instance head; they are automatically in scope. But GHC unhelpfully reports:\r\n\r\n{{{\r\nezyang@sabre:~$ Dev/ghc-7.10.2/usr/bin/ghci A.hs\r\nGHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling A ( A.hs, interpreted )\r\n\r\nA.hs:8:13:\r\n Could not deduce (Show a0)\r\n from the context (Show a)\r\n bound by the type signature for show :: Show a => F a -> String\r\n at A.hs:8:13-45\r\n The type variable ‘a0’ is ambiguous\r\n When checking that:\r\n forall a. Show a => forall a1. Show a1 => F a1 -> String\r\n is more polymorphic than: forall a. Show a => F a -> String\r\n When checking that instance signature for ‘show’\r\n is more general than its signature in the class\r\n Instance sig: forall a.\r\n Show a =>\r\n forall a1. Show a1 => F a1 -> String\r\n Class sig: forall a. Show a => F a -> String\r\n In the instance declaration for ‘Show (F a)’\r\nFailed, modules loaded: none.\r\n}}}\r\n\r\nWhy did I get the wrong idea about how instance signatures work? Well, GHC doesn't warn if you write this:\r\n\r\n{{{\r\ninstance Show a => Show (F a) where\r\n show :: Show a => F a -> String\r\n show (F x) = show x\r\n}}}\r\n\r\nBecause this turns into a full type signature 'Show a, Show a => F a -> String' (the first a and the second a end up getting unified.) I'm not sure if it should warn; it's an easy mistake to make if you are treating instance methods like plain function definitions (of course you have to write the full type signature...)","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11115Indicate missing associated type instances2019-07-07T18:31:53ZrimmingtonIndicate missing associated type instancesIf there is no matching instance for a typeclass that defines an associated type, GHC cannot further reduce an application of that associated type. For nested type family applications, this produces rather large error messages, eg:
```
...If there is no matching instance for a typeclass that defines an associated type, GHC cannot further reduce an application of that associated type. For nested type family applications, this produces rather large error messages, eg:
```
<interactive>:98:20:
Couldn't match type ‘units-2.3:Data.Metrology.Factor.Normalize
(Data.Metrology.Suspicious.Poly.SurfaceUnitFactorsOf
(Data.Singletons.Prelude.Tuple.Snd
(Data.Metrology.Suspicious.Poly.SplitPrefix
(PrefixExp Deci) Deci Core))
units-2.3:Data.Metrology.Factor.@- '['units-2.3:Data.Metrology.Factor.F
Core
('Data.Metrology.Z.S
'Data.Metrology.Z.Zero)])’
with ‘'[]’
In the expression: (25 %> centi Core) `ceilToUnit` deci Core
In an equation for ‘it’:
it = (25 %> centi Core) `ceilToUnit` deci Core
```
The cause of the above error message is that `Deci` is not a member of the typeclass `ExpUnitPrefix` that defines the associated type `PrefixExp`. Unfortunately this is not clear at all from the error message, and adding additional class constraints to the appropriate functions doesn't improve things.
It would be nice if GHC pointed out that there is no `ExpUnitPrefix Deci` instance, or at least that `PrefixExp Deci` cannot be further reduced. I imagine this would be useful for open type families as well, but I can't comment personally.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| Type | FeatureRequest |
| 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":"Indicate missing associated type instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"If there is no matching instance for a typeclass that defines an associated type, GHC cannot further reduce an application of that associated type. For nested type family applications, this produces rather large error messages, eg:\r\n\r\n{{{\r\n<interactive>:98:20:\r\n Couldn't match type ‘units-2.3:Data.Metrology.Factor.Normalize\r\n (Data.Metrology.Suspicious.Poly.SurfaceUnitFactorsOf\r\n (Data.Singletons.Prelude.Tuple.Snd\r\n (Data.Metrology.Suspicious.Poly.SplitPrefix\r\n (PrefixExp Deci) Deci Core))\r\n units-2.3:Data.Metrology.Factor.@- '['units-2.3:Data.Metrology.Factor.F\r\n Core\r\n ('Data.Metrology.Z.S\r\n 'Data.Metrology.Z.Zero)])’\r\n with ‘'[]’\r\n In the expression: (25 %> centi Core) `ceilToUnit` deci Core\r\n In an equation for ‘it’:\r\n it = (25 %> centi Core) `ceilToUnit` deci Core\r\n}}}\r\n\r\nThe cause of the above error message is that `Deci` is not a member of the typeclass `ExpUnitPrefix` that defines the associated type `PrefixExp`. Unfortunately this is not clear at all from the error message, and adding additional class constraints to the appropriate functions doesn't improve things.\r\n\r\nIt would be nice if GHC pointed out that there is no `ExpUnitPrefix Deci` instance, or at least that `PrefixExp Deci` cannot be further reduced. I imagine this would be useful for open type families as well, but I can't comment personally.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/11099Incorrect warning about redundant constraints2019-07-07T18:32:07ZIavor S. DiatchkiIncorrect warning about redundant constraintsThe following program results in an incorrect warning about a redundant constraint:
```
{-# LANGUAGE TypeFamilies #-}
type family SomeFun a
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
f _ = read "HELLO"
```
This is the warning:
...The following program results in an incorrect warning about a redundant constraint:
```
{-# LANGUAGE TypeFamilies #-}
type family SomeFun a
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
f _ = read "HELLO"
```
This is the warning:
```
Redundant constraint: SomeFun i ~ [a]
In the type signature for:
f :: (SomeFun i ~ [a], Read a) => proxy i -> a
```
I tried it on GHC version 7.11.20151029
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Incorrect warning about redundant constraints","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program results in an incorrect warning about a redundant constraint:\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies #-}\r\n\r\ntype family SomeFun a \r\n\r\nf :: (SomeFun i ~ [a], Read a) => proxy i -> a\r\nf _ = read \"HELLO\"\r\n}}}\r\n\r\nThis is the warning:\r\n{{{\r\nRedundant constraint: SomeFun i ~ [a]\r\n In the type signature for:\r\n f :: (SomeFun i ~ [a], Read a) => proxy i -> a\r\n}}}\r\n\r\nI tried it on GHC version 7.11.20151029\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/10978Anonymous type instances2019-07-07T18:32:49Zbenjamin.hodgsonAnonymous type instancesI find that commonly I write a `type family` (because it doesn't *need* to be a `data family`, and `type` families are more flexible), but I find myself writing `data` types for some of the instances anyway.
Presently you're forced to u...I find that commonly I write a `type family` (because it doesn't *need* to be a `data family`, and `type` families are more flexible), but I find myself writing `data` types for some of the instances anyway.
Presently you're forced to use type synonyms for all the instances of a `type family`, even if you don't intend to refer to the type by any name other than that of the type family. I find this tiresome:
```hs
type family F a
type instance F Char = Int
newtype FBool = FBool Int
type instance F Bool = FBool
data FInt = A | B | ...
type instance F Int = FInt
```
**I want to write `data instance`s and `newtype instance`s for `type` families**. These proposed constructs would introduce a new type without a name of its own (the only way to refer to it would be through the `type family`), just like the current design of `data` families. The above code would be roughly equivalent to:
```hs
type family F a
type instance F Char = Int -- already legal
newtype instance F Bool = FBool Int
data instance F Int = A | B | ...
```
I call this idea *anonymous type instances* but I'm open to suggestions for a snappier name.
Going the other way (writing a `type instance` for a `data family`) would remain illegal under this proposal.
```hs
data family G a
type instance G Char = Int -- still illegal
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| Type | FeatureRequest |
| 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":"Anonymous type instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I find that commonly I write a `type family` (because it doesn't ''need'' to be a `data family`, and `type` families are more flexible), but I find myself writing `data` types for some of the instances anyway.\r\n\r\nPresently you're forced to use type synonyms for all the instances of a `type family`, even if you don't intend to refer to the type by any name other than that of the type family. I find this tiresome:\r\n\r\n{{{#!hs\r\ntype family F a\r\n\r\ntype instance F Char = Int\r\n\r\nnewtype FBool = FBool Int\r\ntype instance F Bool = FBool\r\n\r\ndata FInt = A | B | ...\r\ntype instance F Int = FInt\r\n}}}\r\n\r\n'''I want to write `data instance`s and `newtype instance`s for `type` families'''. These proposed constructs would introduce a new type without a name of its own (the only way to refer to it would be through the `type family`), just like the current design of `data` families. The above code would be roughly equivalent to:\r\n\r\n{{{#!hs\r\ntype family F a\r\n\r\ntype instance F Char = Int -- already legal\r\nnewtype instance F Bool = FBool Int\r\ndata instance F Int = A | B | ...\r\n}}}\r\n\r\nI call this idea ''anonymous type instances'' but I'm open to suggestions for a snappier name.\r\n\r\n\r\nGoing the other way (writing a `type instance` for a `data family`) would remain illegal under this proposal.\r\n\r\n{{{#!hs\r\ndata family G a\r\n\r\ntype instance G Char = Int -- still illegal\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/10833Use injective type families (decomposition) when dealing with givens2023-06-12T11:35:15ZJan Stolarekjan.stolarek@ed.ac.ukUse injective type families (decomposition) when dealing with givensConsider this code:
```hs
type family Id a = r | r -> a
id :: (Id a ~ Id b) => a -> b
id x = x
```
GHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints.
And yet ...Consider this code:
```hs
type family Id a = r | r -> a
id :: (Id a ~ Id b) => a -> b
id x = x
```
GHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints.
And yet `Coercion` has a form for representing such coercions, namely "nth" (written `SelCo` in GHC). We could say
```
co : F s1..sn ~ F t1..tn
F is injective in its i'th argument
-----------------------------------
SelCo (Tc i) co : si ~ ti
```
Indeed Lint already accepts such `SelCo`s:
```
lintCoercion the_co@(SelCo cs co)
= do { co' <- lintCoercion co
; let (Pair s t, co_role) = coercionKindRole co'
; if -- forall (both TyVar and CoVar)
...
-- TyCon
| Just (tc_s, tys_s) <- splitTyConApp_maybe s
, Just (tc_t, tys_t) <- splitTyConApp_maybe t
, tc_s == tc_t
, SelTyCon n r0 <- cs
, isInjectiveTyCon tc_s co_role
-- see Note [SelCo and newtypes] in GHC.Core.TyCo.Rep
, tys_s `equalLength` tys_t
, tys_s `lengthExceeds` n
-> do { lintRole the_co (tyConRole co_role tc_s n) r0
; return (SelCo cs co') }
```
Note that `isInjectiveTyCon`! An injective type family is accepted here. (But only if it is injective in *all* arguments, which is stronger than we need.)
Allowing this would be user facing change, hence needing a GHC proposal. But it'd be very simple to implement.
@rae any views on how this might impact soundness?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.2 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #6018 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Use injective type families when dealing with givens","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[6018],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"jstolarek"},"version":"7.10.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Consider this code:\r\n\r\n{{{#!hs\r\ntype family Id a = r | r -> a\r\n\r\nid :: (Id a ~ Id b) => a -> b\r\nid x = x\r\n}}}\r\nGHC currently rejects it because it does not use type family injectivity information when dealing with the given constraints. Implementing this requires changing Core.","type_of_failure":"OtherFailure","blocking":[]} -->Jan Stolarekjan.stolarek@ed.ac.ukJan Stolarekjan.stolarek@ed.ac.ukhttps://gitlab.haskell.org/ghc/ghc/-/issues/10832Generalize injective type families2020-12-09T23:11:31ZJan Stolarekjan.stolarek@ed.ac.ukGeneralize injective type familiesWith injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:
```hs
data Nat = Zero | Succ a
class Add a...With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:
```hs
data Nat = Zero | Succ a
class Add a b r | a b -> r, r a -> b
instance Add Zero b b
instance (Add a b r) => Add (Succ a) b (Succ r)
```
Here we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:
```hs
type family AddTF a b = r | r a -> b where
AddTF Zero b = b
AddTF (Succ a) b = Succ (AddTF a b)
```
But we want to be able to say that.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | FeatureRequest |
| 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":"Generalize injective type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"jstolarek"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say:\r\n\r\n{{{#!hs\r\ndata Nat = Zero | Succ a\r\n\r\nclass Add a b r | a b -> r, r a -> b\r\ninstance Add Zero b b\r\ninstance (Add a b r) => Add (Succ a) b (Succ r)\r\n}}}\r\nHere we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs:\r\n\r\n{{{#!hs\r\ntype family AddTF a b = r | r a -> b where\r\n AddTF Zero b = b\r\n AddTF (Succ a) b = Succ (AddTF a b)\r\n}}}\r\nBut we want to be able to say that.","type_of_failure":"OtherFailure","blocking":[]} -->Jan Stolarekjan.stolarek@ed.ac.ukJan Stolarekjan.stolarek@ed.ac.ukhttps://gitlab.haskell.org/ghc/ghc/-/issues/10776DataKinds promotion of String -> Symbol and Natural -> Nat2020-10-28T13:07:08ZhtebalakaDataKinds promotion of String -> Symbol and Natural -> NatExactly what it says on the tin. It would be nice if the following would compile:
```hs
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
import GHC.TypeLits
import GHC.Natural
data X = X String Natural
data Y :: X -> * where
Y :...Exactly what it says on the tin. It would be nice if the following would compile:
```hs
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
import GHC.TypeLits
import GHC.Natural
data X = X String Natural
data Y :: X -> * where
Y :: Y ('X "hello" 4)
```
I kind of assume there's already a ticket for this, but couldn't find one, so figured I'd open one in case.https://gitlab.haskell.org/ghc/ghc/-/issues/10337One-shot module loops have hard to understand messages2019-07-07T18:36:31ZEdward Z. YangOne-shot module loops have hard to understand messagesConsider these two modules:
```
-- A.hs
module A where
-- B.hs
module B where
import A
```
`ghc --make B.hs` will compile this fine. Now edit `A.hs` to be circular:
```
-- A.hs
module A where
import B
```
and attempt to one-shot com...Consider these two modules:
```
-- A.hs
module A where
-- B.hs
module B where
import A
```
`ghc --make B.hs` will compile this fine. Now edit `A.hs` to be circular:
```
-- A.hs
module A where
import B
```
and attempt to one-shot compile it with `ghc -c A.hs`. You will now get an uninformative error message:
```
A.hs:1:1: Circular imports: module `A' depends on itself
```
You can get a more informative message with `--make`:
```
Module imports form a cycle:
module `A' (A.hs)
imports `B' (./B.hs)
which imports `A' (A.hs)
```
We should either suggest users try again with `--make`, or try harder to give a useful message in one-shot mode.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"One-shot module loops have hard to understand messages","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.11","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider these two modules:\r\n\r\n{{{\r\n-- A.hs\r\nmodule A where\r\n\r\n-- B.hs\r\nmodule B where\r\nimport A\r\n}}}\r\n\r\n`ghc --make B.hs` will compile this fine. Now edit `A.hs` to be circular:\r\n\r\n{{{\r\n-- A.hs\r\nmodule A where\r\nimport B\r\n}}}\r\n\r\nand attempt to one-shot compile it with `ghc -c A.hs`. You will now get an uninformative error message:\r\n\r\n{{{\r\nA.hs:1:1: Circular imports: module `A' depends on itself\r\n}}}\r\n\r\nYou can get a more informative message with `--make`:\r\n\r\n{{{\r\nModule imports form a cycle:\r\n module `A' (A.hs)\r\n imports `B' (./B.hs)\r\n which imports `A' (A.hs)\r\n}}}\r\n\r\nWe should either suggest users try again with `--make`, or try harder to give a useful message in one-shot mode.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/10204Odd interaction between rank-2 types and type families2019-07-07T18:37:06ZIavor S. DiatchkiOdd interaction between rank-2 types and type familiesType inference does not work as expected, when a rank-2 type has a type-family constraint. Consider the following program:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
type family F a
f :: (forall s. (F s ~ Int) =...Type inference does not work as expected, when a rank-2 type has a type-family constraint. Consider the following program:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
type family F a
f :: (forall s. (F s ~ Int) => s -> b) -> b
f _ = undefined
k :: s -> Char
k = undefined
example :: Bool
example = const True (f k)
```
It is rejected with the following error:
```
Couldn't match type ‘b0’ with ‘Char’
‘b0’ is untouchable
inside the constraints (F s ~ Int)
bound by a type expected by the context: (F s ~ Int) => s -> b0
at bug.hs:13:23-25
Expected type: s -> b0
Actual type: s -> Char
In the first argument of ‘f’, namely ‘k’
In the second argument of ‘const’, namely ‘(f k)’
```
This is unexpected because the result of `f` should be the same as
the result of its parameter, and we know the exact type of the parameter, namely `Char`.⊥https://gitlab.haskell.org/ghc/ghc/-/issues/10087DefaultSignatures: error message mentions internal name2020-02-11T12:47:33Zandreas.abelDefaultSignatures: error message mentions internal name```hs
{-# LANGUAGE DefaultSignatures #-}
class C a where
reflexive :: a -> Bool
default reflexive :: Eq a => a -> Bool
reflexive x = x == x
data D
instance C D where
-- /home/abel/play/haskell/bugs/DefaultSig.hs:10:10:
-- N...```hs
{-# LANGUAGE DefaultSignatures #-}
class C a where
reflexive :: a -> Bool
default reflexive :: Eq a => a -> Bool
reflexive x = x == x
data D
instance C D where
-- /home/abel/play/haskell/bugs/DefaultSig.hs:10:10:
-- No instance for (Eq D) arising from a use of ‘Main.$gdmreflexive’
-- In the expression: Main.$gdmreflexive
-- In an equation for ‘reflexive’: reflexive = Main.$gdmreflexive
-- In the instance declaration for ‘C D’
```
Error looks odd: The user has not written $gdmreflexive in his code.
TODO: Better error message.
Maybe this should just trigger a warning that method `reflexive` is undefined for instance `D` of `C`. Like when I remove the default method.
```
/home/abel/play/haskell/bugs/DefaultSig.hs:10:10: Warning:
No explicit implementation for
‘reflexive’
In the instance declaration for ‘C D’
```
It seems the semantics of a default signature is that each instance \*must\* implement this method.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.4 |
| Type | FeatureRequest |
| 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":"DefaultSignatures: error message mentions internal name","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.4","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"{{{#!hs\r\n{-# LANGUAGE DefaultSignatures #-}\r\n\r\nclass C a where\r\n reflexive :: a -> Bool\r\n default reflexive :: Eq a => a -> Bool\r\n reflexive x = x == x\r\n\r\ndata D\r\n\r\ninstance C D where\r\n\r\n-- /home/abel/play/haskell/bugs/DefaultSig.hs:10:10:\r\n-- No instance for (Eq D) arising from a use of ‘Main.$gdmreflexive’\r\n-- In the expression: Main.$gdmreflexive\r\n-- In an equation for ‘reflexive’: reflexive = Main.$gdmreflexive\r\n-- In the instance declaration for ‘C D’\r\n}}}\r\n\r\nError looks odd: The user has not written $gdmreflexive in his code.\r\n\r\nTODO: Better error message.\r\n\r\nMaybe this should just trigger a warning that method {{{reflexive}}} is undefined for instance {{{D}}} of {{{C}}}. Like when I remove the default method. \r\n\r\n{{{\r\n/home/abel/play/haskell/bugs/DefaultSig.hs:10:10: Warning:\r\n No explicit implementation for\r\n ‘reflexive’\r\n In the instance declaration for ‘C D’\r\n}}}\r\n\r\nIt seems the semantics of a default signature is that each instance *must* implement this method.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/9974Allow more general structural recursion without UndecidableInstances2019-07-07T18:38:08ZDavid FeuerAllow more general structural recursion without UndecidableInstancesI bet this is a duplicate, but I couldn't find it.
A simple example from the `HList` package:
```hs
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
type family HRevApp (l1 :: [k]) (l2 :: [k]) :: [k]
type instance HRe...I bet this is a duplicate, but I couldn't find it.
A simple example from the `HList` package:
```hs
{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-}
type family HRevApp (l1 :: [k]) (l2 :: [k]) :: [k]
type instance HRevApp '[] l = l
type instance HRevApp (e ': l) l' = HRevApp l (e ': l')
```
GHC 7.8.3 and 7.11 both complain about the second instance if `UndecidableInstances` is turned off, because the application is no smaller than the index head. Moreover, the same error occurs when the type family is closed. However, GHC already knows how to separate term-level definitions into recursive groups; applying this same analysis to the type family above would reveal that `HRevApp` is structurally recursive, and therefore decidable. It is key, in this case, that the instance for `[]` is visible from the instance declaration for `e ': l`, so such an analysis could only be done in module dependency order for open type families.
Side note: there is a (nasty) workaround available for the problem in this case:
```hs
type family HRevApp' (l1 :: [k]) (l1' :: [k]) (l2 :: [k]) :: [k]
type instance HRevApp' t '[] l = l
type instance HRevApp' (e ': l) (e' ': l') l'' = HRevApp' l l' (e ': l'')
type HRevApp l1 l2 = HRevApp' l1 l1 l2
```https://gitlab.haskell.org/ghc/ghc/-/issues/9898Wanted: higher-order type-level programming2019-07-07T18:38:34ZeriscoWanted: higher-order type-level programming'test3' is expected to type check given that 'test1' and 'test2' type check. 'test4' is not expected to type check.
```
ghc_bug2.hs:24:9:
Couldn't match type `(Char, ())' with `()'
Expected type: Filter (Equal Int) (Char, Filter...'test3' is expected to type check given that 'test1' and 'test2' type check. 'test4' is not expected to type check.
```
ghc_bug2.hs:24:9:
Couldn't match type `(Char, ())' with `()'
Expected type: Filter (Equal Int) (Char, Filter (Equal Int) ())
Actual type: ()
In the expression:
() :: Filter (Equal Int) (Char, Filter (Equal Int) ())
In an equation for `test2':
test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())
ghc_bug2.hs:28:9:
Couldn't match type `(Char, ())' with `()'
Expected type: Filter (Equal Int) (Char, ())
Actual type: ()
In the expression: ()
In an equation for `test3': test3 = ()
```
```hs
{-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds #-}
module Main where
type family Filter f xs where
Filter f (x, xs) = ApplyFilter (f x) (x, Filter f xs)
Filter f () = ()
--
type family ApplyFilter p xs where
ApplyFilter False (x, xs) = xs
ApplyFilter p xs = xs
--
type family Equal x y where
Equal x x = True
Equal x y = False
--
-- Type checks
test1 :: ApplyFilter ((Equal Int) Char) (Char, Filter (Equal Int) ())
test1 = ()
-- Couldn't match type `(Char, ())' with `()'
test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())
-- Couldn't match type `(Char, ())' with `()'
test3 :: Filter (Equal Int) (Char, ())
test3 = ()
-- Type checks, should not
test4 :: Filter (Equal Int) (Char, ())
test4 = ('x', ())
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | Windows |
| Architecture | x86_64 (amd64) |
</details>
<!-- {"blocked_by":[],"summary":"Couldn't match type `(Char, ())' with `()'","status":"New","operating_system":"Windows","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":[],"differentials":[],"test_case":"","architecture":"x86_64 (amd64)","cc":[""],"type":"Bug","description":"'test3' is expected to type check given that 'test1' and 'test2' type check. 'test4' is not expected to type check.\r\n\r\n{{{\r\nghc_bug2.hs:24:9:\r\n Couldn't match type `(Char, ())' with `()'\r\n Expected type: Filter (Equal Int) (Char, Filter (Equal Int) ())\r\n Actual type: ()\r\n In the expression:\r\n () :: Filter (Equal Int) (Char, Filter (Equal Int) ())\r\n In an equation for `test2':\r\n test2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())\r\n\r\nghc_bug2.hs:28:9:\r\n Couldn't match type `(Char, ())' with `()'\r\n Expected type: Filter (Equal Int) (Char, ())\r\n Actual type: ()\r\n In the expression: ()\r\n In an equation for `test3': test3 = ()\r\n}}}\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds #-}\r\nmodule Main where\r\n\r\ntype family Filter f xs where\r\n Filter f (x, xs) = ApplyFilter (f x) (x, Filter f xs)\r\n Filter f () = ()\r\n--\r\n\r\ntype family ApplyFilter p xs where\r\n ApplyFilter False (x, xs) = xs\r\n ApplyFilter p xs = xs\r\n--\r\n\r\ntype family Equal x y where\r\n Equal x x = True\r\n Equal x y = False\r\n--\r\n\r\n-- Type checks\r\ntest1 :: ApplyFilter ((Equal Int) Char) (Char, Filter (Equal Int) ())\r\ntest1 = ()\r\n\r\n-- Couldn't match type `(Char, ())' with `()'\r\ntest2 = () :: Filter (Equal Int) (Char, Filter (Equal Int) ())\r\n\r\n-- Couldn't match type `(Char, ())' with `()'\r\ntest3 :: Filter (Equal Int) (Char, ())\r\ntest3 = ()\r\n\r\n-- Type checks, should not\r\ntest4 :: Filter (Equal Int) (Char, ())\r\ntest4 = ('x', ())\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/9672Error message too long (full case statement printed)2019-07-07T18:39:33Zandreas.abelError message too long (full case statement printed)Imho, it does not make sense to print the other branches of a case when a type error is discovered in one branch. When you see the following example, you will agree with me.
```
src/full/Agda/TypeChecking/Errors.hs:540:35:
Couldn't ...Imho, it does not make sense to print the other branches of a case when a type error is discovered in one branch. When you see the following example, you will agree with me.
```
src/full/Agda/TypeChecking/Errors.hs:540:35:
Couldn't match type ‘[Char]’ with ‘TCMT IO Doc’
Expected type: TCM Doc
Actual type: [Char]
In the expression:
"Module cannot be imported since it has open interaction points"
In a case alternative:
SolvedButOpenHoles
-> "Module cannot be imported since it has open interaction points"
In a stmt of a 'do' block:
```
```hs
case err of {
InternalError s -> panic s
NotImplemented s -> fwords $ "Not implemented: " ++ s
NotSupported s -> fwords $ "Not supported: " ++ s
CompilationError s -> sep [fwords "Compilation error:", text s]
GenericError s -> fwords s
GenericDocError d -> return d
TerminationCheckFailed because
-> fwords
"Termination checking failed for the following functions:"
$$
(nest 2
$ fsep
$ punctuate comma
$ map (pretty . dropTopLevelModule)
$ concatMap termErrFunctions because)
$$ fwords "Problematic calls:"
$$
(nest 2
$ fmap (P.vcat . nub)
$ mapM prettyTCM
$ sortBy (compare `on` callInfoRange)
$ concatMap termErrCalls because)
PropMustBeSingleton
-> fwords
"Datatypes in Prop must have at most one constructor when proof irrelevance is enabled"
DataMustEndInSort t
-> fsep
$ pwords "The type of a datatype must end in a sort."
++ [prettyTCM t] ++ pwords "isn't a sort."
ShouldEndInApplicationOfTheDatatype t
-> fsep
$ pwords
"The target of a constructor must be the datatype applied to its parameters,"
++ [prettyTCM t] ++ pwords "isn't"
ShouldBeAppliedToTheDatatypeParameters s t
-> fsep
$ pwords "The target of the constructor should be"
++ [prettyTCM s] ++ pwords "instead of" ++ [prettyTCM t]
ShouldBeApplicationOf t q
-> fsep
$ pwords "The pattern constructs an element of"
++ [prettyTCM q] ++ pwords "which is not the right datatype"
ShouldBeRecordType t
-> fsep
$ pwords "Expected non-abstract record type, found "
++ [prettyTCM t]
ShouldBeRecordPattern p -> fsep $ pwords "Expected record pattern"
NotAProjectionPattern p
-> fsep
$ pwords "Not a valid projection for a copattern: " ++ [prettyA p]
DifferentArities
-> fwords
"The number of arguments in the defining equations differ"
WrongHidingInLHS -> do { fwords "Unexpected implicit argument" }
WrongHidingInLambda t
-> do { fwords
"Found an implicit lambda where an explicit lambda was expected" }
WrongIrrelevanceInLambda t
-> do { fwords
"Found an irrelevant lambda where a relevant lambda was expected" }
WrongNamedArgument a
-> fsep
$ pwords "Function does not accept argument " ++ [prettyTCM a]
WrongHidingInApplication t
-> do { fwords
"Found an implicit application where an explicit application was expected" }
HidingMismatch h h'
-> fwords
$ "Expected "
++
verbalize (Indefinite h')
++
" argument, but found " ++ verbalize (Indefinite h) ++ " argument"
RelevanceMismatch r r'
-> fwords
$ "Expected "
++
verbalize (Indefinite r')
++
" argument, but found " ++ verbalize (Indefinite r) ++ " argument"
ColorMismatch c c'
-> fsep
$ pwords "Expected argument color to be"
++ [prettyTCM c'] ++ pwords "but found color" ++ [prettyTCM c]
NotInductive t
-> fsep $ [prettyTCM t] ++ pwords "is not an inductive data type"
UninstantiatedDotPattern e
-> fsep $ pwords "Failed to infer the value of dotted pattern"
IlltypedPattern p a -> fsep $ pwords "Type mismatch"
IllformedProjectionPattern p
-> fsep $ pwords "Ill-formed projection pattern " ++ [prettyA p]
CannotEliminateWithPattern p a
-> do { let ...;
fsep
$ pwords "Cannot eliminate type"
++
prettyTCM a
: if isProj then
pwords "with projection pattern" ++ ...
else
pwords "with pattern"
++ prettyA p : pwords "(did you supply too many arguments?)" }
TooManyArgumentsInLHS a
-> fsep
$ pwords
"Left hand side gives too many arguments to a function of type"
++ [prettyTCM a]
WrongNumberOfConstructorArguments c expect given
-> fsep
$ pwords "The constructor"
++
[prettyTCM c]
++
pwords "expects"
++
[text (show expect)]
++
pwords "arguments (including hidden ones), but has been given"
++ [text (show given)] ++ pwords "(including hidden ones)"
CantResolveOverloadedConstructorsTargetingSameDatatype d cs
-> fsep
$ pwords
("Can't resolve overloaded constructors targeting the same datatype ("
++ show (qnameToConcrete d) ++ "):")
++ map pretty cs
DoesNotConstructAnElementOf c t
-> fsep
$ pwords "The constructor"
++
[prettyTCM c]
++ pwords "does not construct an element of" ++ [prettyTCM t]
ConstructorPatternInWrongDatatype c d
-> fsep
$ [prettyTCM c]
++ pwords "is not a constructor of the datatype" ++ [prettyTCM d]
IndicesNotConstructorApplications [i]
-> fwords "The index" $$ nest 2 (prettyTCM i)
$$
fsep
(pwords "is not a constructor (or literal) applied to variables"
++ pwords "(note that parameters count as constructor arguments)")
IndicesNotConstructorApplications is
-> fwords "The indices" $$ nest 2 (vcat $ map prettyTCM is)
$$
fsep
(pwords "are not constructors (or literals) applied to variables"
++ pwords "(note that parameters count as constructor arguments)")
IndexVariablesNotDistinct vs is
-> fwords "The variables"
$$ nest 2 (vcat $ map (\ v -> prettyTCM (I.Var v [])) vs)
$$ fwords "in the indices"
$$ nest 2 (vcat $ map prettyTCM is)
$$
fwords
"are not distinct (note that parameters count as constructor arguments)"
IndicesFreeInParameters vs indices pars
-> fwords "The variables"
$$ nest 2 (vcat $ map (\ v -> prettyTCM (I.Var v [])) vs)
$$
fwords
"which are used (perhaps as constructor parameters) in the index expressions"
$$ nest 2 (vcat $ map prettyTCM indices)
$$ fwords "are free in the parameters"
$$ nest 2 (vcat $ map prettyTCM pars)
ShadowedModule x []
-> (throwImpossible
(Impossible "src/full/Agda/TypeChecking/Errors.hs" 404))
ShadowedModule x ms@(m : _)
-> fsep
$ pwords "Duplicate definition of module"
++
[prettyTCM x <> text "."]
++
pwords "Previous definition of"
++
[help m]
++ pwords "module" ++ [prettyTCM x] ++ pwords "at" ++ [prettyTCM r]
where
help m = do { ... }
r = case ... of {
[] -> ...
r : _ -> ... }
defSiteOfLast [] = noRange
defSiteOfLast ns = nameBindingSite (last ns)
ModuleArityMismatch m EmptyTel args
-> fsep
$ pwords "The module"
++
[prettyTCM m]
++ pwords "is not parameterized, but is being applied to arguments"
ModuleArityMismatch m tel@(ExtendTel _ _) args
-> fsep
$ pwords "The arguments to "
++
[prettyTCM m]
++ pwords "does not fit the telescope" ++ [prettyTCM tel]
ShouldBeEmpty t []
-> fsep
$ [prettyTCM t]
++ pwords "should be empty, but that's not obvious to me"
ShouldBeEmpty t ps
-> fsep
([prettyTCM t]
++
pwords
"should be empty, but the following constructor patterns are valid:")
$$ nest 2 (vcat $ map (showPat 0) ps)
ShouldBeASort t
-> fsep $ [prettyTCM t] ++ pwords "should be a sort, but it isn't"
ShouldBePi t
-> fsep
$ [prettyTCM t] ++ pwords "should be a function type, but it isn't"
NotAProperTerm -> fwords "Found a malformed term"
SetOmegaNotValidType -> fwords "Set\969 is not a valid type"
InvalidType v
-> fsep $ [prettyTCM v] ++ pwords "is not a valid type"
SplitOnIrrelevant p t
-> fsep
$ pwords "Cannot pattern match"
++ [prettyA p] ++ pwords "against irrelevant type" ++ [prettyTCM t]
DefinitionIsIrrelevant x
-> fsep
$ text "Identifier"
: prettyTCM x
: pwords "is declared irrelevant, so it cannot be used here"
VariableIsIrrelevant x
-> fsep
$ text "Variable"
: prettyTCM x
: pwords "is declared irrelevant, so it cannot be used here"
UnequalBecauseOfUniverseConflict cmp s t
-> fsep $ [prettyTCM s, notCmp cmp, ....]
UnequalTerms cmp s t a
-> do { (d1, d2, d) <- prettyInEqual s t;
fsep $ [...] ++ pwords "of type" ++ [...] ++ [...] }
UnequalTypes cmp a b -> prettyUnequal a (notCmp cmp) b
UnequalColors a b -> error "TODO guilhem 4"
HeterogeneousEquality u a v b
-> fsep
$ pwords "Refuse to solve heterogeneous constraint"
++
[prettyTCM u]
++
pwords ":"
++
[prettyTCM a]
++ pwords "=?=" ++ [prettyTCM v] ++ pwords ":" ++ [prettyTCM b]
UnequalRelevance cmp a b
-> fsep
$ [prettyTCM a, notCmp cmp, ....]
++
pwords
"because one is a relevant function type and the other is an irrelevant function type"
UnequalHiding a b
-> fsep
$ [prettyTCM a, text "!=", ....]
++
pwords
"because one is an implicit function type and the other is an explicit function type"
UnequalSorts s1 s2 -> fsep $ [prettyTCM s1, text "!=", ....]
NotLeqSort s1 s2
-> fsep
$ pwords
"The type of the constructor does not fit in the sort of the datatype, since"
++
[prettyTCM s1]
++ pwords "is not less or equal than" ++ [prettyTCM s2]
TooFewFields r xs
-> fsep
$ pwords "Missing fields"
++
punctuate comma (map pretty xs)
++ pwords "in an element of the record" ++ [prettyTCM r]
TooManyFields r xs
-> fsep
$ pwords "The record type"
++
[prettyTCM r]
++
pwords "does not have the fields"
++ punctuate comma (map pretty xs)
DuplicateConstructors xs
-> fsep
$ pwords "Duplicate constructors"
++ punctuate comma (map pretty xs) ++ pwords "in datatype"
DuplicateFields xs
-> fsep
$ pwords "Duplicate fields"
++ punctuate comma (map pretty xs) ++ pwords "in record"
UnexpectedWithPatterns ps
-> fsep
$ pwords "Unexpected with patterns"
++ (punctuate (text " |") $ map prettyA ps)
WithClausePatternMismatch p q
-> fsep
$ pwords "With clause pattern "
++
[prettyA p]
++
pwords " is not an instance of its parent pattern "
++ [prettyTCM q]
MetaCannotDependOn m ps i
-> fsep
$ pwords "The metavariable"
++
[prettyTCM $ MetaV m []]
++
pwords "cannot depend on"
++ [pvar i] ++ pwords "because it" ++ deps
where
pvar = prettyTCM . var
deps
= case map pvar ps of {
[] -> ...
[x] -> ...
xs -> ... }
MetaOccursInItself m
-> fsep
$ pwords "Cannot construct infinite solution of metavariable"
++ [prettyTCM $ MetaV m []]
BuiltinMustBeConstructor s e
-> fsep
$ [prettyA e]
++
pwords "must be a constructor in the binding to builtin"
++ [text s]
NoSuchBuiltinName s
-> fsep $ pwords "There is no built-in thing called" ++ [text s]
DuplicateBuiltinBinding b x y
-> fsep
$ pwords "Duplicate binding for built-in thing"
++
[text b <> comma] ++ pwords "previous binding to" ++ [prettyTCM x]
NoBindingForBuiltin x
-> fsep
$ pwords "No binding for builtin thing"
++
[text x <> comma]
++
pwords
("use {-# BUILTIN " ++ x ++ " name #-} to bind it to 'name'")
NoSuchPrimitiveFunction x
-> fsep
$ pwords "There is no primitive function called" ++ [text x]
BuiltinInParameterisedModule x
-> fwords
$ "The BUILTIN pragma cannot appear inside a bound context "
++
"(for instance, in a parameterised module or as a local declaration)"
IllegalLetInTelescope tb
-> fsep
$ [pretty tb] ++ pwords " is not allowed in a telescope here."
NoRHSRequiresAbsurdPattern ps
-> fwords
$ "The right-hand side can only be omitted if there "
++ "is an absurd pattern, () or {}, in the left-hand side."
AbsurdPatternRequiresNoRHS ps
-> fwords
$ "The right-hand side must be omitted if there "
++ "is an absurd pattern, () or {}, in the left-hand side."
LocalVsImportedModuleClash m
-> fsep
$ pwords "The module"
++
[text $ show m]
++
pwords "can refer to either a local module or an imported module"
SolvedButOpenHoles
-> "Module cannot be imported since it has open interaction points"
UnsolvedMetas rs
-> fsep (pwords "Unsolved metas at the following locations:")
$$ nest 2 (vcat $ map prettyTCM rs)
UnsolvedConstraints cs
-> fsep (pwords "Failed to solve the following constraints:")
$$ nest 2 (vcat $ map prettyConstraint cs)
where
prettyConstraint :: ProblemConstraint -> TCM Doc
prettyConstraint c
= f (prettyTCM c)
where
r = ...
....
CyclicModuleDependency ms
-> fsep (pwords "cyclic module dependency:")
$$ nest 2 (vcat $ map pretty ms)
FileNotFound x files
-> fsep
(pwords "Failed to find source of module"
++ [pretty x] ++ pwords "in any of the following locations:")
$$ nest 2 (vcat $ map (text . filePath) files)
OverlappingProjects f m1 m2
-> fsep
(pwords "The file"
++
[text (filePath f)]
++
pwords "can be accessed via several project roots. Both"
++
[pretty m1]
++ pwords "and" ++ [pretty m2] ++ pwords "point to this file.")
AmbiguousTopLevelModuleName x files
-> fsep
(pwords "Ambiguous module name. The module name"
++
[pretty x] ++ pwords "could refer to any of the following files:")
$$ nest 2 (vcat $ map (text . filePath) files)
ClashingFileNamesFor x files
-> fsep
(pwords "Multiple possible sources for module"
++ [text $ show x] ++ pwords "found:")
$$ nest 2 (vcat $ map (text . filePath) files)
ModuleDefinedInOtherFile mod file file'
-> fsep
$ pwords "You tried to load"
++
[text (filePath file)]
++
pwords "which defines the module"
++
[pretty mod <> text "."]
++
pwords "However, according to the include path this module should"
++ pwords "be defined in" ++ [text (filePath file') <> text "."]
ModuleNameDoesntMatchFileName given files
-> fsep
(pwords
"The name of the top level module does not match the file name. The module"
++
[pretty given]
++ pwords "should be defined in one of the following files:")
$$ nest 2 (vcat $ map (text . filePath) files)
BothWithAndRHS -> fsep $ pwords "Unexpected right hand side"
NotInScope xs
-> fsep (pwords "Not in scope:") $$ nest 2 (vcat $ map name xs)
where
name x = fsep [...]
suggestion s
| elem ':' s = parens $ text "did you forget space around the ':'?"
| elem "->" two
= parens $ text "did you forget space around the '->'?"
| otherwise = empty
where
two = ...
NoSuchModule x -> fsep $ pwords "No such module" ++ [pretty x]
AmbiguousName x ys
-> vcat
[fsep
$ pwords "Ambiguous name"
++ [...] ++ pwords "It could refer to any one of",
nest 2 $ vcat $ map nameWithBinding ys, ....]
AmbiguousModule x ys
-> vcat
[fsep
$ pwords "Ambiguous module name"
++ [...] ++ pwords "It could refer to any one of",
nest 2 $ vcat $ map help ys, ....]
where
help :: ModuleName -> TCM Doc
help m = do { ... }
UninstantiatedModule x
-> fsep
(pwords "Cannot access the contents of the parameterised module"
++
[pretty x <> text "."]
++
pwords
"To do this the module first has to be instantiated. For instance:")
$$ nest 2 (hsep [text "module", pretty x <> text "'", ....])
ClashingDefinition x y
-> fsep
$ pwords "Multiple definitions of"
++
[pretty x <> text "."]
++
pwords "Previous definition at"
++ [prettyTCM $ nameBindingSite $ qnameName y]
ClashingModule m1 m2
-> fsep
$ pwords "The modules"
++ [prettyTCM m1, text "and", ....] ++ pwords "clash."
ClashingImport x y
-> fsep
$ pwords "Import clash between" ++ [pretty x, text "and", ....]
ClashingModuleImport x y
-> fsep
$ pwords "Module import clash between"
++ [pretty x, text "and", ....]
PatternShadowsConstructor x c
-> fsep
$ pwords "The pattern variable"
++
[prettyTCM x]
++ pwords "has the same name as the constructor" ++ [prettyTCM c]
DuplicateImports m xs
-> fsep
$ pwords "Ambiguous imports from module"
++ [pretty m] ++ pwords "for" ++ punctuate comma (map pretty xs)
ModuleDoesntExport m xs
-> fsep
$ pwords "The module"
++
[pretty m]
++
pwords "doesn't export the following:"
++ punctuate comma (map pretty xs)
NotAModuleExpr e
-> fsep
$ pwords
"The right-hand side of a module definition must have the form 'M e1 .. en'"
++
pwords "where M is a module name. The expression"
++ [pretty e, text "doesn't."]
FieldOutsideRecord
-> fsep $ pwords "Field appearing outside record declaration."
InvalidPattern p
-> fsep $ pretty p : pwords "is not a valid pattern"
RepeatedVariablesInPattern xs
-> fsep
$ pwords "Repeated variables in left hand side:" ++ map pretty xs
NotAnExpression e
-> fsep $ [pretty e] ++ pwords "is not a valid expression."
NotAValidLetBinding nd -> fwords $ "Not a valid let-declaration"
NothingAppliedToHiddenArg e
-> fsep
$ [pretty e]
++
pwords "cannot appear by itself. It needs to be the argument to"
++ pwords "a function expecting an implicit argument."
NothingAppliedToInstanceArg e
-> fsep
$ [pretty e]
++
pwords "cannot appear by itself. It needs to be the argument to"
++ pwords "a function expecting an instance argument."
NoParseForApplication es
-> fsep
$ pwords "Could not parse the application"
++ [pretty $ C.RawApp noRange es]
AmbiguousParseForApplication es es'
-> fsep
(pwords "Don't know how to parse"
++ [pretty_es <> (text ".")] ++ pwords "Could mean any one of:")
$$ nest 2 (vcat $ map pretty' es')
where
pretty_es :: TCM Doc
pretty_es = pretty $ C.RawApp noRange es
pretty' :: C.Expr -> TCM Doc
....
BadArgumentsToPatternSynonym x
-> fsep
$ pwords "Bad arguments to pattern synonym " ++ [prettyTCM x]
TooFewArgumentsToPatternSynonym x
-> fsep
$ pwords "Too few arguments to pattern synonym " ++ [prettyTCM x]
UnusedVariableInPatternSynonym
-> fsep $ pwords "Unused variable in pattern synonym."
NoParseForLHS IsLHS p
-> fsep $ pwords "Could not parse the left-hand side" ++ [pretty p]
NoParseForLHS IsPatSyn p
-> fsep
$ pwords "Could not parse the pattern synonym" ++ [pretty p]
AmbiguousParseForLHS lhsOrPatSyn p ps
-> fsep
(pwords "Don't know how to parse"
++ [pretty_p <> text "."] ++ pwords "Could mean any one of:")
$$ nest 2 (vcat $ map pretty' ps)
where
pretty_p :: TCM Doc
pretty_p = pretty p
pretty' :: C.Pattern -> TCM Doc
....
IncompletePatternMatching v args
-> fsep
$ pwords "Incomplete pattern matching for"
++
[prettyTCM v <> text "."]
++ pwords "No match for" ++ map prettyTCM args
UnreachableClauses f pss
-> fsep
$ pwords "Unreachable" ++ pwords (plural (length pss) "clause")
where
plural 1 thing = thing
plural n thing = thing ++ "s"
CoverageFailure f pss
-> fsep
(pwords "Incomplete pattern matching for"
++ [prettyTCM f <> text "."] ++ pwords "Missing cases:")
$$ nest 2 (vcat $ map display pss)
where
display ps = do { ... }
nicify f ps = do { ... }
CoverageCantSplitOn c tel cIxs gIxs
| length cIxs /= length gIxs
-> (throwImpossible
(Impossible "src/full/Agda/TypeChecking/Errors.hs" 750))
| otherwise
-> addCtxTel tel
$ vcat
([fsep
$ pwords
"I'm not sure if there should be a case for the constructor"
++
[...]
++
pwords "because I get stuck when trying to solve the following"
++
pwords
"unification problems (inferred index \8799 expected index):"]
++
zipWith
(\ c g -> nest 2 $ prettyTCM c <+> text "\8799" <+> prettyTCM g)
cIxs
gIxs)
CoverageCantSplitIrrelevantType a
-> fsep
$ pwords "Cannot split on argument of irrelevant datatype"
++ [prettyTCM a]
CoverageCantSplitType a
-> fsep
$ pwords "Cannot split on argument of non-datatype"
++ [prettyTCM a]
SplitError e -> prettyTCM e
WithoutKError a u v
-> fsep
$ pwords "Cannot eliminate reflexive equation"
++
[prettyTCM u]
++
pwords "="
++
[prettyTCM v]
++
pwords "of type"
++ [prettyTCM a] ++ pwords "because K has been disabled."
NotStrictlyPositive d ocs
-> fsep
$ pwords "The datatype"
++
[prettyTCM d]
++ pwords "is not strictly positive, because" ++ prettyOcc "it" ocs
where
prettyOcc _ [] = []
prettyOcc it (OccCon d c r : ocs) = concat [...]
prettyOcc it (OccClause f n r : ocs) = concat [...]
prettyR NonPositively = pwords "negatively"
prettyR (ArgumentTo i q)
= pwords "as the" ++ [...] ++ pwords "argument to" ++ [...]
th 0 = text "first"
th 1 = text "second"
th 2 = text "third"
th n = text (show $ n - 1) <> text "th"
....
IFSNoCandidateInScope t
-> fsep
$ pwords "No variable of type"
++ [prettyTCM t] ++ pwords "was found in scope."
SafeFlagPostulate e
-> fsep
$ pwords "Cannot postulate"
++ [pretty e] ++ pwords "with safe flag"
SafeFlagPragma xs
-> let
plural
| length xs == 1 = ...
| otherwise = ...
in
fsep
$ [fwords ("Cannot set OPTION pragma" ++ plural)]
++ map text xs ++ [fwords "with safe flag."]
SafeFlagNoTerminationCheck
-> fsep
(pwords "Cannot use NO_TERMINATION_CHECK pragma with safe flag.")
SafeFlagNonTerminating
-> fsep
(pwords "Cannot use NON_TERMINATING pragma with safe flag.")
SafeFlagTerminating
-> fsep (pwords "Cannot use TERMINATING pragma with safe flag.")
SafeFlagPrimTrustMe
-> fsep (pwords "Cannot use primTrustMe with safe flag")
NeedOptionCopatterns
-> fsep
(pwords
"Option --copatterns needed to enable destructor patterns") }
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.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":"Error message too long (full case statement printed)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Imho, it does not make sense to print the other branches of a case when a type error is discovered in one branch. When you see the following example, you will agree with me.\r\n{{{\r\nsrc/full/Agda/TypeChecking/Errors.hs:540:35:\r\n Couldn't match type ‘[Char]’ with ‘TCMT IO Doc’\r\n Expected type: TCM Doc\r\n Actual type: [Char]\r\n In the expression:\r\n \"Module cannot be imported since it has open interaction points\"\r\n In a case alternative:\r\n SolvedButOpenHoles\r\n -> \"Module cannot be imported since it has open interaction points\"\r\n In a stmt of a 'do' block:\r\n}}}\r\n{{{#!hs\r\n case err of {\r\n InternalError s -> panic s\r\n NotImplemented s -> fwords $ \"Not implemented: \" ++ s\r\n NotSupported s -> fwords $ \"Not supported: \" ++ s\r\n CompilationError s -> sep [fwords \"Compilation error:\", text s]\r\n GenericError s -> fwords s\r\n GenericDocError d -> return d\r\n TerminationCheckFailed because\r\n -> fwords\r\n \"Termination checking failed for the following functions:\"\r\n $$\r\n (nest 2\r\n $ fsep\r\n $ punctuate comma\r\n $ map (pretty . dropTopLevelModule)\r\n $ concatMap termErrFunctions because)\r\n $$ fwords \"Problematic calls:\"\r\n $$\r\n (nest 2\r\n $ fmap (P.vcat . nub)\r\n $ mapM prettyTCM\r\n $ sortBy (compare `on` callInfoRange)\r\n $ concatMap termErrCalls because)\r\n PropMustBeSingleton\r\n -> fwords\r\n \"Datatypes in Prop must have at most one constructor when proof irrelevance is enabled\"\r\n DataMustEndInSort t\r\n -> fsep\r\n $ pwords \"The type of a datatype must end in a sort.\"\r\n ++ [prettyTCM t] ++ pwords \"isn't a sort.\"\r\n ShouldEndInApplicationOfTheDatatype t\r\n -> fsep\r\n $ pwords\r\n \"The target of a constructor must be the datatype applied to its parameters,\"\r\n ++ [prettyTCM t] ++ pwords \"isn't\"\r\n ShouldBeAppliedToTheDatatypeParameters s t\r\n -> fsep\r\n $ pwords \"The target of the constructor should be\"\r\n ++ [prettyTCM s] ++ pwords \"instead of\" ++ [prettyTCM t]\r\n ShouldBeApplicationOf t q\r\n -> fsep\r\n $ pwords \"The pattern constructs an element of\"\r\n ++ [prettyTCM q] ++ pwords \"which is not the right datatype\"\r\n ShouldBeRecordType t\r\n -> fsep\r\n $ pwords \"Expected non-abstract record type, found \"\r\n ++ [prettyTCM t]\r\n ShouldBeRecordPattern p -> fsep $ pwords \"Expected record pattern\"\r\n NotAProjectionPattern p\r\n -> fsep\r\n $ pwords \"Not a valid projection for a copattern: \" ++ [prettyA p]\r\n DifferentArities\r\n -> fwords\r\n \"The number of arguments in the defining equations differ\"\r\n WrongHidingInLHS -> do { fwords \"Unexpected implicit argument\" }\r\n WrongHidingInLambda t\r\n -> do { fwords\r\n \"Found an implicit lambda where an explicit lambda was expected\" }\r\n WrongIrrelevanceInLambda t\r\n -> do { fwords\r\n \"Found an irrelevant lambda where a relevant lambda was expected\" }\r\n WrongNamedArgument a\r\n -> fsep\r\n $ pwords \"Function does not accept argument \" ++ [prettyTCM a]\r\n WrongHidingInApplication t\r\n -> do { fwords\r\n \"Found an implicit application where an explicit application was expected\" }\r\n HidingMismatch h h'\r\n -> fwords\r\n $ \"Expected \"\r\n ++\r\n verbalize (Indefinite h')\r\n ++\r\n \" argument, but found \" ++ verbalize (Indefinite h) ++ \" argument\"\r\n RelevanceMismatch r r'\r\n -> fwords\r\n $ \"Expected \"\r\n ++\r\n verbalize (Indefinite r')\r\n ++\r\n \" argument, but found \" ++ verbalize (Indefinite r) ++ \" argument\"\r\n ColorMismatch c c'\r\n -> fsep\r\n $ pwords \"Expected argument color to be\"\r\n ++ [prettyTCM c'] ++ pwords \"but found color\" ++ [prettyTCM c]\r\n NotInductive t\r\n -> fsep $ [prettyTCM t] ++ pwords \"is not an inductive data type\"\r\n UninstantiatedDotPattern e\r\n -> fsep $ pwords \"Failed to infer the value of dotted pattern\"\r\n IlltypedPattern p a -> fsep $ pwords \"Type mismatch\"\r\n IllformedProjectionPattern p\r\n -> fsep $ pwords \"Ill-formed projection pattern \" ++ [prettyA p]\r\n CannotEliminateWithPattern p a\r\n -> do { let ...;\r\n fsep\r\n $ pwords \"Cannot eliminate type\"\r\n ++\r\n prettyTCM a\r\n : if isProj then\r\n pwords \"with projection pattern\" ++ ...\r\n else\r\n pwords \"with pattern\"\r\n ++ prettyA p : pwords \"(did you supply too many arguments?)\" }\r\n TooManyArgumentsInLHS a\r\n -> fsep\r\n $ pwords\r\n \"Left hand side gives too many arguments to a function of type\"\r\n ++ [prettyTCM a]\r\n WrongNumberOfConstructorArguments c expect given\r\n -> fsep\r\n $ pwords \"The constructor\"\r\n ++\r\n [prettyTCM c]\r\n ++\r\n pwords \"expects\"\r\n ++\r\n [text (show expect)]\r\n ++\r\n pwords \"arguments (including hidden ones), but has been given\"\r\n ++ [text (show given)] ++ pwords \"(including hidden ones)\"\r\n CantResolveOverloadedConstructorsTargetingSameDatatype d cs\r\n -> fsep\r\n $ pwords\r\n (\"Can't resolve overloaded constructors targeting the same datatype (\"\r\n ++ show (qnameToConcrete d) ++ \"):\")\r\n ++ map pretty cs\r\n DoesNotConstructAnElementOf c t\r\n -> fsep\r\n $ pwords \"The constructor\"\r\n ++\r\n [prettyTCM c]\r\n ++ pwords \"does not construct an element of\" ++ [prettyTCM t]\r\n ConstructorPatternInWrongDatatype c d\r\n -> fsep\r\n $ [prettyTCM c]\r\n ++ pwords \"is not a constructor of the datatype\" ++ [prettyTCM d]\r\n IndicesNotConstructorApplications [i]\r\n -> fwords \"The index\" $$ nest 2 (prettyTCM i)\r\n $$\r\n fsep\r\n (pwords \"is not a constructor (or literal) applied to variables\"\r\n ++ pwords \"(note that parameters count as constructor arguments)\")\r\n IndicesNotConstructorApplications is\r\n -> fwords \"The indices\" $$ nest 2 (vcat $ map prettyTCM is)\r\n $$\r\n fsep\r\n (pwords \"are not constructors (or literals) applied to variables\"\r\n ++ pwords \"(note that parameters count as constructor arguments)\")\r\n IndexVariablesNotDistinct vs is\r\n -> fwords \"The variables\"\r\n $$ nest 2 (vcat $ map (\\ v -> prettyTCM (I.Var v [])) vs)\r\n $$ fwords \"in the indices\"\r\n $$ nest 2 (vcat $ map prettyTCM is)\r\n $$\r\n fwords\r\n \"are not distinct (note that parameters count as constructor arguments)\"\r\n IndicesFreeInParameters vs indices pars\r\n -> fwords \"The variables\"\r\n $$ nest 2 (vcat $ map (\\ v -> prettyTCM (I.Var v [])) vs)\r\n $$\r\n fwords\r\n \"which are used (perhaps as constructor parameters) in the index expressions\"\r\n $$ nest 2 (vcat $ map prettyTCM indices)\r\n $$ fwords \"are free in the parameters\"\r\n $$ nest 2 (vcat $ map prettyTCM pars)\r\n ShadowedModule x []\r\n -> (throwImpossible\r\n (Impossible \"src/full/Agda/TypeChecking/Errors.hs\" 404))\r\n ShadowedModule x ms@(m : _)\r\n -> fsep\r\n $ pwords \"Duplicate definition of module\"\r\n ++\r\n [prettyTCM x <> text \".\"]\r\n ++\r\n pwords \"Previous definition of\"\r\n ++\r\n [help m]\r\n ++ pwords \"module\" ++ [prettyTCM x] ++ pwords \"at\" ++ [prettyTCM r]\r\n where\r\n help m = do { ... }\r\n r = case ... of {\r\n [] -> ...\r\n r : _ -> ... }\r\n defSiteOfLast [] = noRange\r\n defSiteOfLast ns = nameBindingSite (last ns)\r\n ModuleArityMismatch m EmptyTel args\r\n -> fsep\r\n $ pwords \"The module\"\r\n ++\r\n [prettyTCM m]\r\n ++ pwords \"is not parameterized, but is being applied to arguments\"\r\n ModuleArityMismatch m tel@(ExtendTel _ _) args\r\n -> fsep\r\n $ pwords \"The arguments to \"\r\n ++\r\n [prettyTCM m]\r\n ++ pwords \"does not fit the telescope\" ++ [prettyTCM tel]\r\n ShouldBeEmpty t []\r\n -> fsep\r\n $ [prettyTCM t]\r\n ++ pwords \"should be empty, but that's not obvious to me\"\r\n ShouldBeEmpty t ps\r\n -> fsep\r\n ([prettyTCM t]\r\n ++\r\n pwords\r\n \"should be empty, but the following constructor patterns are valid:\")\r\n $$ nest 2 (vcat $ map (showPat 0) ps)\r\n ShouldBeASort t\r\n -> fsep $ [prettyTCM t] ++ pwords \"should be a sort, but it isn't\"\r\n ShouldBePi t\r\n -> fsep\r\n $ [prettyTCM t] ++ pwords \"should be a function type, but it isn't\"\r\n NotAProperTerm -> fwords \"Found a malformed term\"\r\n SetOmegaNotValidType -> fwords \"Set\\969 is not a valid type\"\r\n InvalidType v\r\n -> fsep $ [prettyTCM v] ++ pwords \"is not a valid type\"\r\n SplitOnIrrelevant p t\r\n -> fsep\r\n $ pwords \"Cannot pattern match\"\r\n ++ [prettyA p] ++ pwords \"against irrelevant type\" ++ [prettyTCM t]\r\n DefinitionIsIrrelevant x\r\n -> fsep\r\n $ text \"Identifier\"\r\n : prettyTCM x\r\n : pwords \"is declared irrelevant, so it cannot be used here\"\r\n VariableIsIrrelevant x\r\n -> fsep\r\n $ text \"Variable\"\r\n : prettyTCM x\r\n : pwords \"is declared irrelevant, so it cannot be used here\"\r\n UnequalBecauseOfUniverseConflict cmp s t\r\n -> fsep $ [prettyTCM s, notCmp cmp, ....]\r\n UnequalTerms cmp s t a\r\n -> do { (d1, d2, d) <- prettyInEqual s t;\r\n fsep $ [...] ++ pwords \"of type\" ++ [...] ++ [...] }\r\n UnequalTypes cmp a b -> prettyUnequal a (notCmp cmp) b\r\n UnequalColors a b -> error \"TODO guilhem 4\"\r\n HeterogeneousEquality u a v b\r\n -> fsep\r\n $ pwords \"Refuse to solve heterogeneous constraint\"\r\n ++\r\n [prettyTCM u]\r\n ++\r\n pwords \":\"\r\n ++\r\n [prettyTCM a]\r\n ++ pwords \"=?=\" ++ [prettyTCM v] ++ pwords \":\" ++ [prettyTCM b]\r\n UnequalRelevance cmp a b\r\n -> fsep\r\n $ [prettyTCM a, notCmp cmp, ....]\r\n ++\r\n pwords\r\n \"because one is a relevant function type and the other is an irrelevant function type\"\r\n UnequalHiding a b\r\n -> fsep\r\n $ [prettyTCM a, text \"!=\", ....]\r\n ++\r\n pwords\r\n \"because one is an implicit function type and the other is an explicit function type\"\r\n UnequalSorts s1 s2 -> fsep $ [prettyTCM s1, text \"!=\", ....]\r\n NotLeqSort s1 s2\r\n -> fsep\r\n $ pwords\r\n \"The type of the constructor does not fit in the sort of the datatype, since\"\r\n ++\r\n [prettyTCM s1]\r\n ++ pwords \"is not less or equal than\" ++ [prettyTCM s2]\r\n TooFewFields r xs\r\n -> fsep\r\n $ pwords \"Missing fields\"\r\n ++\r\n punctuate comma (map pretty xs)\r\n ++ pwords \"in an element of the record\" ++ [prettyTCM r]\r\n TooManyFields r xs\r\n -> fsep\r\n $ pwords \"The record type\"\r\n ++\r\n [prettyTCM r]\r\n ++\r\n pwords \"does not have the fields\"\r\n ++ punctuate comma (map pretty xs)\r\n DuplicateConstructors xs\r\n -> fsep\r\n $ pwords \"Duplicate constructors\"\r\n ++ punctuate comma (map pretty xs) ++ pwords \"in datatype\"\r\n DuplicateFields xs\r\n -> fsep\r\n $ pwords \"Duplicate fields\"\r\n ++ punctuate comma (map pretty xs) ++ pwords \"in record\"\r\n UnexpectedWithPatterns ps\r\n -> fsep\r\n $ pwords \"Unexpected with patterns\"\r\n ++ (punctuate (text \" |\") $ map prettyA ps)\r\n WithClausePatternMismatch p q\r\n -> fsep\r\n $ pwords \"With clause pattern \"\r\n ++\r\n [prettyA p]\r\n ++\r\n pwords \" is not an instance of its parent pattern \"\r\n ++ [prettyTCM q]\r\n MetaCannotDependOn m ps i\r\n -> fsep\r\n $ pwords \"The metavariable\"\r\n ++\r\n [prettyTCM $ MetaV m []]\r\n ++\r\n pwords \"cannot depend on\"\r\n ++ [pvar i] ++ pwords \"because it\" ++ deps\r\n where\r\n pvar = prettyTCM . var\r\n deps\r\n = case map pvar ps of {\r\n [] -> ...\r\n [x] -> ...\r\n xs -> ... }\r\n MetaOccursInItself m\r\n -> fsep\r\n $ pwords \"Cannot construct infinite solution of metavariable\"\r\n ++ [prettyTCM $ MetaV m []]\r\n BuiltinMustBeConstructor s e\r\n -> fsep\r\n $ [prettyA e]\r\n ++\r\n pwords \"must be a constructor in the binding to builtin\"\r\n ++ [text s]\r\n NoSuchBuiltinName s\r\n -> fsep $ pwords \"There is no built-in thing called\" ++ [text s]\r\n DuplicateBuiltinBinding b x y\r\n -> fsep\r\n $ pwords \"Duplicate binding for built-in thing\"\r\n ++\r\n [text b <> comma] ++ pwords \"previous binding to\" ++ [prettyTCM x]\r\n NoBindingForBuiltin x\r\n -> fsep\r\n $ pwords \"No binding for builtin thing\"\r\n ++\r\n [text x <> comma]\r\n ++\r\n pwords\r\n (\"use {-# BUILTIN \" ++ x ++ \" name #-} to bind it to 'name'\")\r\n NoSuchPrimitiveFunction x\r\n -> fsep\r\n $ pwords \"There is no primitive function called\" ++ [text x]\r\n BuiltinInParameterisedModule x\r\n -> fwords\r\n $ \"The BUILTIN pragma cannot appear inside a bound context \"\r\n ++\r\n \"(for instance, in a parameterised module or as a local declaration)\"\r\n IllegalLetInTelescope tb\r\n -> fsep\r\n $ [pretty tb] ++ pwords \" is not allowed in a telescope here.\"\r\n NoRHSRequiresAbsurdPattern ps\r\n -> fwords\r\n $ \"The right-hand side can only be omitted if there \"\r\n ++ \"is an absurd pattern, () or {}, in the left-hand side.\"\r\n AbsurdPatternRequiresNoRHS ps\r\n -> fwords\r\n $ \"The right-hand side must be omitted if there \"\r\n ++ \"is an absurd pattern, () or {}, in the left-hand side.\"\r\n LocalVsImportedModuleClash m\r\n -> fsep\r\n $ pwords \"The module\"\r\n ++\r\n [text $ show m]\r\n ++\r\n pwords \"can refer to either a local module or an imported module\"\r\n SolvedButOpenHoles\r\n -> \"Module cannot be imported since it has open interaction points\"\r\n UnsolvedMetas rs\r\n -> fsep (pwords \"Unsolved metas at the following locations:\")\r\n $$ nest 2 (vcat $ map prettyTCM rs)\r\n UnsolvedConstraints cs\r\n -> fsep (pwords \"Failed to solve the following constraints:\")\r\n $$ nest 2 (vcat $ map prettyConstraint cs)\r\n where\r\n prettyConstraint :: ProblemConstraint -> TCM Doc\r\n prettyConstraint c\r\n = f (prettyTCM c)\r\n where\r\n r = ...\r\n ....\r\n CyclicModuleDependency ms\r\n -> fsep (pwords \"cyclic module dependency:\")\r\n $$ nest 2 (vcat $ map pretty ms)\r\n FileNotFound x files\r\n -> fsep\r\n (pwords \"Failed to find source of module\"\r\n ++ [pretty x] ++ pwords \"in any of the following locations:\")\r\n $$ nest 2 (vcat $ map (text . filePath) files)\r\n OverlappingProjects f m1 m2\r\n -> fsep\r\n (pwords \"The file\"\r\n ++\r\n [text (filePath f)]\r\n ++\r\n pwords \"can be accessed via several project roots. Both\"\r\n ++\r\n [pretty m1]\r\n ++ pwords \"and\" ++ [pretty m2] ++ pwords \"point to this file.\")\r\n AmbiguousTopLevelModuleName x files\r\n -> fsep\r\n (pwords \"Ambiguous module name. The module name\"\r\n ++\r\n [pretty x] ++ pwords \"could refer to any of the following files:\")\r\n $$ nest 2 (vcat $ map (text . filePath) files)\r\n ClashingFileNamesFor x files\r\n -> fsep\r\n (pwords \"Multiple possible sources for module\"\r\n ++ [text $ show x] ++ pwords \"found:\")\r\n $$ nest 2 (vcat $ map (text . filePath) files)\r\n ModuleDefinedInOtherFile mod file file'\r\n -> fsep\r\n $ pwords \"You tried to load\"\r\n ++\r\n [text (filePath file)]\r\n ++\r\n pwords \"which defines the module\"\r\n ++\r\n [pretty mod <> text \".\"]\r\n ++\r\n pwords \"However, according to the include path this module should\"\r\n ++ pwords \"be defined in\" ++ [text (filePath file') <> text \".\"]\r\n ModuleNameDoesntMatchFileName given files\r\n -> fsep\r\n (pwords\r\n \"The name of the top level module does not match the file name. The module\"\r\n ++\r\n [pretty given]\r\n ++ pwords \"should be defined in one of the following files:\")\r\n $$ nest 2 (vcat $ map (text . filePath) files)\r\n BothWithAndRHS -> fsep $ pwords \"Unexpected right hand side\"\r\n NotInScope xs\r\n -> fsep (pwords \"Not in scope:\") $$ nest 2 (vcat $ map name xs)\r\n where\r\n name x = fsep [...]\r\n suggestion s\r\n | elem ':' s = parens $ text \"did you forget space around the ':'?\"\r\n | elem \"->\" two\r\n = parens $ text \"did you forget space around the '->'?\"\r\n | otherwise = empty\r\n where\r\n two = ...\r\n NoSuchModule x -> fsep $ pwords \"No such module\" ++ [pretty x]\r\n AmbiguousName x ys\r\n -> vcat\r\n [fsep\r\n $ pwords \"Ambiguous name\"\r\n ++ [...] ++ pwords \"It could refer to any one of\",\r\n nest 2 $ vcat $ map nameWithBinding ys, ....]\r\n AmbiguousModule x ys\r\n -> vcat\r\n [fsep\r\n $ pwords \"Ambiguous module name\"\r\n ++ [...] ++ pwords \"It could refer to any one of\",\r\n nest 2 $ vcat $ map help ys, ....]\r\n where\r\n help :: ModuleName -> TCM Doc\r\n help m = do { ... }\r\n UninstantiatedModule x\r\n -> fsep\r\n (pwords \"Cannot access the contents of the parameterised module\"\r\n ++\r\n [pretty x <> text \".\"]\r\n ++\r\n pwords\r\n \"To do this the module first has to be instantiated. For instance:\")\r\n $$ nest 2 (hsep [text \"module\", pretty x <> text \"'\", ....])\r\n ClashingDefinition x y\r\n -> fsep\r\n $ pwords \"Multiple definitions of\"\r\n ++\r\n [pretty x <> text \".\"]\r\n ++\r\n pwords \"Previous definition at\"\r\n ++ [prettyTCM $ nameBindingSite $ qnameName y]\r\n ClashingModule m1 m2\r\n -> fsep\r\n $ pwords \"The modules\"\r\n ++ [prettyTCM m1, text \"and\", ....] ++ pwords \"clash.\"\r\n ClashingImport x y\r\n -> fsep\r\n $ pwords \"Import clash between\" ++ [pretty x, text \"and\", ....]\r\n ClashingModuleImport x y\r\n -> fsep\r\n $ pwords \"Module import clash between\"\r\n ++ [pretty x, text \"and\", ....]\r\n PatternShadowsConstructor x c\r\n -> fsep\r\n $ pwords \"The pattern variable\"\r\n ++\r\n [prettyTCM x]\r\n ++ pwords \"has the same name as the constructor\" ++ [prettyTCM c]\r\n DuplicateImports m xs\r\n -> fsep\r\n $ pwords \"Ambiguous imports from module\"\r\n ++ [pretty m] ++ pwords \"for\" ++ punctuate comma (map pretty xs)\r\n ModuleDoesntExport m xs\r\n -> fsep\r\n $ pwords \"The module\"\r\n ++\r\n [pretty m]\r\n ++\r\n pwords \"doesn't export the following:\"\r\n ++ punctuate comma (map pretty xs)\r\n NotAModuleExpr e\r\n -> fsep\r\n $ pwords\r\n \"The right-hand side of a module definition must have the form 'M e1 .. en'\"\r\n ++\r\n pwords \"where M is a module name. The expression\"\r\n ++ [pretty e, text \"doesn't.\"]\r\n FieldOutsideRecord\r\n -> fsep $ pwords \"Field appearing outside record declaration.\"\r\n InvalidPattern p\r\n -> fsep $ pretty p : pwords \"is not a valid pattern\"\r\n RepeatedVariablesInPattern xs\r\n -> fsep\r\n $ pwords \"Repeated variables in left hand side:\" ++ map pretty xs\r\n NotAnExpression e\r\n -> fsep $ [pretty e] ++ pwords \"is not a valid expression.\"\r\n NotAValidLetBinding nd -> fwords $ \"Not a valid let-declaration\"\r\n NothingAppliedToHiddenArg e\r\n -> fsep\r\n $ [pretty e]\r\n ++\r\n pwords \"cannot appear by itself. It needs to be the argument to\"\r\n ++ pwords \"a function expecting an implicit argument.\"\r\n NothingAppliedToInstanceArg e\r\n -> fsep\r\n $ [pretty e]\r\n ++\r\n pwords \"cannot appear by itself. It needs to be the argument to\"\r\n ++ pwords \"a function expecting an instance argument.\"\r\n NoParseForApplication es\r\n -> fsep\r\n $ pwords \"Could not parse the application\"\r\n ++ [pretty $ C.RawApp noRange es]\r\n AmbiguousParseForApplication es es'\r\n -> fsep\r\n (pwords \"Don't know how to parse\"\r\n ++ [pretty_es <> (text \".\")] ++ pwords \"Could mean any one of:\")\r\n $$ nest 2 (vcat $ map pretty' es')\r\n where\r\n pretty_es :: TCM Doc\r\n pretty_es = pretty $ C.RawApp noRange es\r\n pretty' :: C.Expr -> TCM Doc\r\n ....\r\n BadArgumentsToPatternSynonym x\r\n -> fsep\r\n $ pwords \"Bad arguments to pattern synonym \" ++ [prettyTCM x]\r\n TooFewArgumentsToPatternSynonym x\r\n -> fsep\r\n $ pwords \"Too few arguments to pattern synonym \" ++ [prettyTCM x]\r\n UnusedVariableInPatternSynonym\r\n -> fsep $ pwords \"Unused variable in pattern synonym.\"\r\n NoParseForLHS IsLHS p\r\n -> fsep $ pwords \"Could not parse the left-hand side\" ++ [pretty p]\r\n NoParseForLHS IsPatSyn p\r\n -> fsep\r\n $ pwords \"Could not parse the pattern synonym\" ++ [pretty p]\r\n AmbiguousParseForLHS lhsOrPatSyn p ps\r\n -> fsep\r\n (pwords \"Don't know how to parse\"\r\n ++ [pretty_p <> text \".\"] ++ pwords \"Could mean any one of:\")\r\n $$ nest 2 (vcat $ map pretty' ps)\r\n where\r\n pretty_p :: TCM Doc\r\n pretty_p = pretty p\r\n pretty' :: C.Pattern -> TCM Doc\r\n ....\r\n IncompletePatternMatching v args\r\n -> fsep\r\n $ pwords \"Incomplete pattern matching for\"\r\n ++\r\n [prettyTCM v <> text \".\"]\r\n ++ pwords \"No match for\" ++ map prettyTCM args\r\n UnreachableClauses f pss\r\n -> fsep\r\n $ pwords \"Unreachable\" ++ pwords (plural (length pss) \"clause\")\r\n where\r\n plural 1 thing = thing\r\n plural n thing = thing ++ \"s\"\r\n CoverageFailure f pss\r\n -> fsep\r\n (pwords \"Incomplete pattern matching for\"\r\n ++ [prettyTCM f <> text \".\"] ++ pwords \"Missing cases:\")\r\n $$ nest 2 (vcat $ map display pss)\r\n where\r\n display ps = do { ... }\r\n nicify f ps = do { ... }\r\n CoverageCantSplitOn c tel cIxs gIxs\r\n | length cIxs /= length gIxs\r\n -> (throwImpossible\r\n (Impossible \"src/full/Agda/TypeChecking/Errors.hs\" 750))\r\n | otherwise\r\n -> addCtxTel tel\r\n $ vcat\r\n ([fsep\r\n $ pwords\r\n \"I'm not sure if there should be a case for the constructor\"\r\n ++\r\n [...]\r\n ++\r\n pwords \"because I get stuck when trying to solve the following\"\r\n ++\r\n pwords\r\n \"unification problems (inferred index \\8799 expected index):\"]\r\n ++\r\n zipWith\r\n (\\ c g -> nest 2 $ prettyTCM c <+> text \"\\8799\" <+> prettyTCM g)\r\n cIxs\r\n gIxs)\r\n CoverageCantSplitIrrelevantType a\r\n -> fsep\r\n $ pwords \"Cannot split on argument of irrelevant datatype\"\r\n ++ [prettyTCM a]\r\n CoverageCantSplitType a\r\n -> fsep\r\n $ pwords \"Cannot split on argument of non-datatype\"\r\n ++ [prettyTCM a]\r\n SplitError e -> prettyTCM e\r\n WithoutKError a u v\r\n -> fsep\r\n $ pwords \"Cannot eliminate reflexive equation\"\r\n ++\r\n [prettyTCM u]\r\n ++\r\n pwords \"=\"\r\n ++\r\n [prettyTCM v]\r\n ++\r\n pwords \"of type\"\r\n ++ [prettyTCM a] ++ pwords \"because K has been disabled.\"\r\n NotStrictlyPositive d ocs\r\n -> fsep\r\n $ pwords \"The datatype\"\r\n ++\r\n [prettyTCM d]\r\n ++ pwords \"is not strictly positive, because\" ++ prettyOcc \"it\" ocs\r\n where\r\n prettyOcc _ [] = []\r\n prettyOcc it (OccCon d c r : ocs) = concat [...]\r\n prettyOcc it (OccClause f n r : ocs) = concat [...]\r\n prettyR NonPositively = pwords \"negatively\"\r\n prettyR (ArgumentTo i q)\r\n = pwords \"as the\" ++ [...] ++ pwords \"argument to\" ++ [...]\r\n th 0 = text \"first\"\r\n th 1 = text \"second\"\r\n th 2 = text \"third\"\r\n th n = text (show $ n - 1) <> text \"th\"\r\n ....\r\n IFSNoCandidateInScope t\r\n -> fsep\r\n $ pwords \"No variable of type\"\r\n ++ [prettyTCM t] ++ pwords \"was found in scope.\"\r\n SafeFlagPostulate e\r\n -> fsep\r\n $ pwords \"Cannot postulate\"\r\n ++ [pretty e] ++ pwords \"with safe flag\"\r\n SafeFlagPragma xs\r\n -> let\r\n plural\r\n | length xs == 1 = ...\r\n | otherwise = ...\r\n in\r\n fsep\r\n $ [fwords (\"Cannot set OPTION pragma\" ++ plural)]\r\n ++ map text xs ++ [fwords \"with safe flag.\"]\r\n SafeFlagNoTerminationCheck\r\n -> fsep\r\n (pwords \"Cannot use NO_TERMINATION_CHECK pragma with safe flag.\")\r\n SafeFlagNonTerminating\r\n -> fsep\r\n (pwords \"Cannot use NON_TERMINATING pragma with safe flag.\")\r\n SafeFlagTerminating\r\n -> fsep (pwords \"Cannot use TERMINATING pragma with safe flag.\")\r\n SafeFlagPrimTrustMe\r\n -> fsep (pwords \"Cannot use primTrustMe with safe flag\")\r\n NeedOptionCopatterns\r\n -> fsep\r\n (pwords\r\n \"Option --copatterns needed to enable destructor patterns\") }\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->nadinenadinehttps://gitlab.haskell.org/ghc/ghc/-/issues/9667Type inference is weaker for GADT than analogous Data Family2019-07-07T18:39:35ZCarter SchonwaldType inference is weaker for GADT than analogous Data FamilyI'm marking this as a Feature request rather than a bug (though it was unexpected behavior for me!)
In my code base i had the following types
```hs
data Prod = Pair Prod Prod | Unit
data VProd (vect :: * -> * ) (prd:: Prod ) val ...I'm marking this as a Feature request rather than a bug (though it was unexpected behavior for me!)
In my code base i had the following types
```hs
data Prod = Pair Prod Prod | Unit
data VProd (vect :: * -> * ) (prd:: Prod ) val where
VLeaf :: !(v a) -> VProd v Unit a
VPair :: !(VProd v pra a) -> !(VProd v prb b ) ->VProd v (Pair pra prb) (a,b)
data MVProd (vect :: * -> * -> * ) (prd:: Prod ) (st :: * ) val where
MVLeaf :: !(mv st a) -> MVProd mv Unit st a
MVPair :: !(MVProd mv pra st a) -> !(MVProd mv prb st b ) -> MVProd mv (Pair pra prb) st (a,b)
```
which are meant as a way of modeling vectors of tuples as tuples (err trees) of vectors
however, sometimes type inference would fail in explosive ways
like
```
*Numerical.Data.Vector.Pair Data.Vector VG> (VPair (VLeaf (va :: Vector Int)) (VLeaf (vb:: Vector Int))) <- return $ VG.fromList [(1::Int,2::Int),(3,5)] :: (VProd Vector (Pair Unit Unit) (Int,Int))
<interactive>:24:16:
Could not deduce (a ~ Int)
from the context (t1 ~ 'Pair pra prb, t2 ~ (a, b))
bound by a pattern with constructor
VPair :: forall (v :: * -> *) (pra :: Prod) a (prb :: Prod) b.
VProd v pra a -> VProd v prb b -> VProd v ('Pair pra prb) (a, b),
in a pattern binding in
interactive GHCi command
at <interactive>:24:2-59
or from (pra ~ 'Unit)
bound by a pattern with constructor
VLeaf :: forall (v :: * -> *) a. v a -> VProd v 'Unit a,
in a pattern binding in
interactive GHCi command
at <interactive>:24:9-32
‘a’ is a rigid type variable bound by
a pattern with constructor
VPair :: forall (v :: * -> *) (pra :: Prod) a (prb :: Prod) b.
VProd v pra a -> VProd v prb b -> VProd v ('Pair pra prb) (a, b),
in a pattern binding in
interactive GHCi command
at <interactive>:24:2
Expected type: t0 a
Actual type: Vector Int
In the pattern: va :: Vector Int
In the pattern: VLeaf (va :: Vector Int)
In the pattern:
VPair (VLeaf (va :: Vector Int)) (VLeaf (vb :: Vector Int))
<interactive>:24:43:
Could not deduce (b ~ Int)
from the context (t1 ~ 'Pair pra prb, t2 ~ (a, b))
bound by a pattern with constructor
VPair :: forall (v :: * -> *) (pra :: Prod) a (prb :: Prod) b.
VProd v pra a -> VProd v prb b -> VProd v ('Pair pra prb) (a, b),
in a pattern binding in
interactive GHCi command
at <interactive>:24:2-59
or from (pra ~ 'Unit)
bound by a pattern with constructor
VLeaf :: forall (v :: * -> *) a. v a -> VProd v 'Unit a,
in a pattern binding in
interactive GHCi command
at <interactive>:24:9-32
or from (prb ~ 'Unit)
bound by a pattern with constructor
VLeaf :: forall (v :: * -> *) a. v a -> VProd v 'Unit a,
in a pattern binding in
interactive GHCi command
at <interactive>:24:36-58
‘b’ is a rigid type variable bound by
a pattern with constructor
VPair :: forall (v :: * -> *) (pra :: Prod) a (prb :: Prod) b.
VProd v pra a -> VProd v prb b -> VProd v ('Pair pra prb) (a, b),
in a pattern binding in
interactive GHCi command
at <interactive>:24:2
Expected type: t0 b
Actual type: Vector Int
In the pattern: vb :: Vector Int
In the pattern: VLeaf (vb :: Vector Int)
In the pattern:
VPair (VLeaf (va :: Vector Int)) (VLeaf (vb :: Vector Int))
<interactive>:24:65:
Couldn't match type ‘(Int, Int)’ with ‘Int’
Expected type: VProd Vector ('Pair 'Unit 'Unit) (Int, Int)
Actual type: VProd Vector ('Pair 'Unit 'Unit) (Int, (Int, Int))
In the first argument of ‘GHC.GHCi.ghciStepIO ::
IO a_a5BR -> IO a_a5BR’, namely
‘return $ VG.fromList [(1 :: Int, 2 :: Int), (3, 5)] ::
VProd Vector (Pair Unit Unit) (Int, Int)’
In a stmt of an interactive GHCi command:
(VPair (VLeaf (va :: Vector Int))
(VLeaf (vb :: Vector Int))) <- GHC.GHCi.ghciStepIO ::
IO a_a5BR -> IO a_a5BR
(return $ VG.fromList [(1 :: Int, 2 :: Int), (3, 5)] ::
VProd Vector (Pair Unit Unit) (Int, Int))
<interactive>:24:65:
Couldn't match expected type ‘IO (VProd t0 t1 t2)’
with actual type ‘VProd Vector ('Pair 'Unit 'Unit) (Int, Int)’
In the first argument of ‘GHC.GHCi.ghciStepIO ::
IO a_a5BR -> IO a_a5BR’, namely
‘return $ VG.fromList [(1 :: Int, 2 :: Int), (3, 5)] ::
VProd Vector (Pair Unit Unit) (Int, Int)’
In a stmt of an interactive GHCi command:
(VPair (VLeaf (va :: Vector Int))
(VLeaf (vb :: Vector Int))) <- GHC.GHCi.ghciStepIO ::
IO a_a5BR -> IO a_a5BR
(return $ VG.fromList [(1 :: Int, 2 :: Int), (3, 5)] ::
VProd Vector (Pair Unit Unit) (Int, Int))
```
I then experimented with using Data Families instead
```hs
data Prod = Pair Prod Prod | Unit
data family VProd (vect :: * -> * ) (prd:: Prod ) val -- where
data instance VProd v Unit a where
VLeaf :: !(v a) -> VProd v Unit a
data instance VProd v (Pair pra prb ) (a,b) where
VPair :: !(VProd v pra a) -> !(VProd v prb b ) ->VProd v (Pair pra prb) (a,b)
data family MVProd (vect :: * -> * -> * ) (prd:: Prod ) (st :: * ) val -- where
data instance MVProd mv Unit st a where
MVLeaf :: !(mv st a) -> MVProd mv Unit st a
data instance MVProd mv (Pair pra prb) st (a,b) where
MVPair :: !(MVProd mv pra st a) -> !(MVProd mv prb st b ) -> MVProd mv (Pair pra prb) st (a,b)
```
and type inference would chug along quite happily on the same example.
Attached is the file needed to (somewhat minimally) reproduce this
I guess what I'm saying here is I've quite a funny tension, I'm writing a patently closed data type, which has a perfectly reasonable GADT definition, but I need to use an (Open!) data family definition to get good type inference in the use sites!
This seems like something where (roughly) when the GADT constructors satisfy something analogous to the no overlap condition of a valid data family, similarly strong type inference might be possible?
I'm not sure if this makes sense, so i'm posing it as a feature request because i'm Not quite sure what the implications would be within type inference, but it'd probably be quite nice for end users because they'd suddenly get much better type inference for a large class of GADTs (i think)https://gitlab.haskell.org/ghc/ghc/-/issues/9624"Unlikely constraint" recognition2019-07-07T18:39:46ZDavid Feuer"Unlikely constraint" recognitionSome constraints or combinations are relatively unlikely to appear in correct code, or at least correct code written by beginners. A few tiny examples:
```hs
(Integral a, Fractional a) => -- Possible, but rare, in correct code.
(Integr...Some constraints or combinations are relatively unlikely to appear in correct code, or at least correct code written by beginners. A few tiny examples:
```hs
(Integral a, Fractional a) => -- Possible, but rare, in correct code.
(Integral a, RealFloat a) => -- Rather less possible in correct code.
(Num a, Foldable a) => -- Possible, but unlikely for a beginner.
(Fractional [a]) =>
(Show (A -> B)) =>
```
The current error messages when constraints like these are not satisfied does nothing to suggest that they are unlikely to be correct or to explain to a beginner what kinds of mistakes can lead to errors like this. I imagine some people who teach classes using Haskell will have an idea of which specific things are worth singling out for a special explanation.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.8.3 |
| Type | FeatureRequest |
| 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":"\"Unlikely constraint\" recognition","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Some constraints or combinations are relatively unlikely to appear in correct code, or at least correct code written by beginners. A few tiny examples:\r\n\r\n{{{#!hs\r\n(Integral a, Fractional a) => -- Possible, but rare, in correct code.\r\n(Integral a, RealFloat a) => -- Rather less possible in correct code.\r\n(Num a, Foldable a) => -- Possible, but unlikely for a beginner.\r\n(Fractional [a]) =>\r\n(Show (A -> B)) =>\r\n}}}\r\n\r\nThe current error messages when constraints like these are not satisfied does nothing to suggest that they are unlikely to be correct or to explain to a beginner what kinds of mistakes can lead to errors like this. I imagine some people who teach classes using Haskell will have an idea of which specific things are worth singling out for a special explanation.","type_of_failure":"OtherFailure","blocking":[]} -->