GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:35:52Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/10450Poor type error message when an argument is insufficently polymorphic2019-07-07T18:35:52ZsjcjoostenPoor type error message when an argument is insufficently polymorphicWhen pattern matching, "let/where" and "case" have different behaviours.
Currently, this is accepted (a version using 'where' instead of 'let' type-checks too):
```hs
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Main where
...When pattern matching, "let/where" and "case" have different behaviours.
Currently, this is accepted (a version using 'where' instead of 'let' type-checks too):
```hs
{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
module Main where
data Phantom x = Phantom Int deriving Show
foo :: forall y. (forall x. (Phantom x)) -> Phantom y
foo (Phantom x) = Phantom (x+1)
-- trying to map foo over a list, this is the only way I can get it to work
typeAnnotatedMap :: (forall x. [Phantom x])
-> [Phantom y]
typeAnnotatedMap intList = case intList of
[] -> []
_ -> let (phead:ptail) = intList
in foo phead : typeAnnotatedMap ptail
```
The following are not accepted:
```hs
typeAnnotatedMap1 :: (forall x. [Phantom x])
-> [Phantom y]
typeAnnotatedMap1 intList = case intList of
[] -> []
(phead:ptail) -> foo phead : typeAnnotatedMap1 ptail
typeAnnotatedMap2 :: (forall x. [Phantom x])
-> [Phantom y]
typeAnnotatedMap2 [] = []
typeAnnotatedMap2 (phead:ptail) = foo phead : typeAnnotatedMap2 ptail
```
The current type error is something like:
```
Couldn't match type ‘x0’ with ‘x’
because type variable ‘x’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: [Phantom x]
```
More helpful would be something like:
```
Your pattern match bound the following types to a shared skolem variable:
ptail :: [Phantom x0] (bound at rankNtest.hs:11:25)
phead :: Phantom x0 (bound at rankNtest.hs:11:19)
You may have intended to use a "let" or "where" pattern-match instead.
```https://gitlab.haskell.org/ghc/ghc/-/issues/10341hs-boot files can have bogus declarations if they're not exported2019-07-07T18:36:30ZEdward Z. Yanghs-boot files can have bogus declarations if they're not exportedConsider:
```
-- A.hs-boot
module A(foo) where
foo :: A -> Int
data A = AC { bar :: Int } | CC
-- NB: A is not exported
-- B.hs
module B where
import {-# SOURCE #-} A
-- A.hs
module A(foo) where
import B
data A = AC { ...Consider:
```
-- A.hs-boot
module A(foo) where
foo :: A -> Int
data A = AC { bar :: Int } | CC
-- NB: A is not exported
-- B.hs
module B where
import {-# SOURCE #-} A
-- A.hs
module A(foo) where
import B
data A = AC { foo :: Int } | BC
```
GHC won't complain that `A` is incompatibly defined, since it's not exported.
Seems relatively harmless though.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/10150Suppress orphan instance warning per instance2019-07-07T18:37:19ZEdward Z. YangSuppress orphan instance warning per instanceIn the same way we have overlapping/incoherent instance pragmas which can be applied on a per instance basis, it would be good to have a `-fno-warn-orphan-instance` pragma which can be applied on a per-instance basis.
Annoyingly, there ...In the same way we have overlapping/incoherent instance pragmas which can be applied on a per instance basis, it would be good to have a `-fno-warn-orphan-instance` pragma which can be applied on a per-instance basis.
Annoyingly, there is not an obvious syntax to use for this case, since SOP for a module with orphan instances is `{-# GHC_OPTIONS -fno-warn-orphans #-}`
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.11 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Suppress orphan instance warning per instance","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":"FeatureRequest","description":"In the same way we have overlapping/incoherent instance pragmas which can be applied on a per instance basis, it would be good to have a `-fno-warn-orphan-instance` pragma which can be applied on a per-instance basis.\r\n\r\nAnnoyingly, there is not an obvious syntax to use for this case, since SOP for a module with orphan instances is `{-# GHC_OPTIONS -fno-warn-orphans #-}`","type_of_failure":"OtherFailure","blocking":[]} -->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/9981Potential typechecker regression in GHC 7.10.1RC2019-07-07T18:38:04ZHerbert Valerio Riedelhvr@gnu.orgPotential typechecker regression in GHC 7.10.1RCThe following snippet (extracted from hackage:index-core) is accepted by GHCs prior to GHC 7.10:
```hs
{-# LANGUAGE Rank2Types, TypeOperators #-}
module Foo where
type a :-> b = forall i . a i -> b i
class IFunctor f where
fmapI ...The following snippet (extracted from hackage:index-core) is accepted by GHCs prior to GHC 7.10:
```hs
{-# LANGUAGE Rank2Types, TypeOperators #-}
module Foo where
type a :-> b = forall i . a i -> b i
class IFunctor f where
fmapI :: (a :-> b) -> (f a :-> f b)
class (IFunctor m) => IMonad m where
returnI :: a :-> m a
bindI :: (a :-> m b) -> (m a :-> m b)
(?>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i
(?>=) = flip bindI
```
```
$ ghci-7.8.4 -Wall Foo.hs
GHCi, version 7.8.4: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Control.IMonad.Core ( Foo.hs, interpreted )
Ok, modules loaded: Control.IMonad.Core.
λ:2> :browse
type (:->) (a :: * -> *) (b :: * -> *) = forall i. a i -> b i
class IFunctor (f :: (* -> *) -> * -> *) where
fmapI :: (a :-> b) -> f a :-> f b
class IFunctor m => IMonad (m :: (* -> *) -> * -> *) where
returnI :: a i -> m a i
bindI :: (a :-> m b) -> m a :-> m b
(?>=) :: IMonad m => m a i -> (a :-> m b) -> m b i
```
vs.
```
$ ghci-7.10.0.20141227 -Wall Foo.hs
GHCi, version 7.10.0.20141227: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Control.IMonad.Core ( Foo.hs, interpreted )
Foo.hs:15:14:
Couldn't match type ‘a i0 -> m b i0’ with ‘forall i1. a i1 -> m b i1’
Expected type: (a i0 -> m b i0) -> m a i -> m b i
Actual type: a :-> m b -> m a i -> m b i
Relevant bindings include (?>=) :: m a i -> a :-> m b -> m b i (bound at Foo.hs:15:1)
In the first argument of ‘flip’, namely ‘bindI’
In the expression: flip bindI
Failed, modules loaded: none.
λ:2>
```
I'm not sure though whether that module was valid to begin with...
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.10.1-rc1 |
| Type | Bug |
| TypeOfFailure | ValidProgramRejected |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Potential typechecker regression in GHC 7.10.1RC","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"simonpj"},"version":"7.10.1-rc1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following snippet (extracted from hackage:index-core) is accepted by GHCs prior to GHC 7.10:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE Rank2Types, TypeOperators #-}\r\n\r\nmodule Foo where\r\n\r\ntype a :-> b = forall i . a i -> b i\r\n\r\nclass IFunctor f where\r\n fmapI :: (a :-> b) -> (f a :-> f b)\r\n\r\nclass (IFunctor m) => IMonad m where\r\n returnI :: a :-> m a\r\n bindI :: (a :-> m b) -> (m a :-> m b)\r\n\r\n(?>=) :: (IMonad m) => m a i -> (a :-> m b) -> m b i\r\n(?>=) = flip bindI\r\n}}}\r\n\r\n{{{\r\n$ ghci-7.8.4 -Wall Foo.hs \r\nGHCi, version 7.8.4: http://www.haskell.org/ghc/ :? for help\r\nLoading package ghc-prim ... linking ... done.\r\nLoading package integer-gmp ... linking ... done.\r\nLoading package base ... linking ... done.\r\n[1 of 1] Compiling Control.IMonad.Core ( Foo.hs, interpreted )\r\nOk, modules loaded: Control.IMonad.Core.\r\nλ:2> :browse\r\ntype (:->) (a :: * -> *) (b :: * -> *) = forall i. a i -> b i\r\nclass IFunctor (f :: (* -> *) -> * -> *) where\r\n fmapI :: (a :-> b) -> f a :-> f b\r\nclass IFunctor m => IMonad (m :: (* -> *) -> * -> *) where\r\n returnI :: a i -> m a i\r\n bindI :: (a :-> m b) -> m a :-> m b\r\n(?>=) :: IMonad m => m a i -> (a :-> m b) -> m b i\r\n}}}\r\n\r\nvs.\r\n\r\n{{{\r\n$ ghci-7.10.0.20141227 -Wall Foo.hs \r\nGHCi, version 7.10.0.20141227: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Control.IMonad.Core ( Foo.hs, interpreted )\r\n\r\nFoo.hs:15:14:\r\n Couldn't match type ‘a i0 -> m b i0’ with ‘forall i1. a i1 -> m b i1’\r\n Expected type: (a i0 -> m b i0) -> m a i -> m b i\r\n Actual type: a :-> m b -> m a i -> m b i\r\n Relevant bindings include (?>=) :: m a i -> a :-> m b -> m b i (bound at Foo.hs:15:1)\r\n In the first argument of ‘flip’, namely ‘bindI’\r\n In the expression: flip bindI\r\nFailed, modules loaded: none.\r\nλ:2> \r\n}}}\r\n\r\nI'm not sure though whether that module was valid to begin with...","type_of_failure":"ValidProgramRejected","blocking":[]} -->8.4.1Simon Peyton JonesSimon Peyton Joneshttps://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/9756Warn about unnecessary unsafeCoerce2019-07-07T18:39:11ZDavid FeuerWarn about unnecessary unsafeCoerce`unsafeCoerce` has been around a lot longer than `coerce`, so older code tends to use it even if `coerce` could do the job. It would be nice if the type checker could produce a warning when it detected such a situation.
<details><summar...`unsafeCoerce` has been around a lot longer than `coerce`, so older code tends to use it even if `coerce` could do the job. It would be nice if the type checker could produce a warning when it detected such a situation.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.9 |
| 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":"Warn about unnecessary unsafeCoerce","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.9","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"`unsafeCoerce` has been around a lot longer than `coerce`, so older code tends to use it even if `coerce` could do the job. It would be nice if the type checker could produce a warning when it detected such a situation.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/9717More lazy orphan module loading2022-05-05T04:40:34ZEdward Z. YangMore lazy orphan module loadingCurrently, when we import a module, we eagerly load all of the orphan modules transitively reachable from it (TcRnDriver:tcRnImports). This is a bit of bummer: as module import hierarchies get deeper and deeper, we'll collect more and mo...Currently, when we import a module, we eagerly load all of the orphan modules transitively reachable from it (TcRnDriver:tcRnImports). This is a bit of bummer: as module import hierarchies get deeper and deeper, we'll collect more and more orphan instances and load more and more modules eagerly.
The idea is to try to arrange for an orphan module not to be loaded, unless we think that it might have a relevant instance. Instead of just recording a list of orphan modules transitively reachable from a module, we will also record a digest of what type classes and types the orphan provides instances for. (This will be similar to the data we record for `ifInstTys` in `IfaceClsInst`.)
Now, when we do any operation involving instances, we check and see if there are also orphans which could provide relevant instances (based on the digest) and load those. If an instance could never have been used, we avoid loading its interface file entirely.
This doesn't appear to help too much for type families, where we have to load all of the instances anyway in order to check for consistency.
A choice to make: Should we record just the class, or also the types involved? It would be best if we could quickly conclude that there are no more instances to load, but this may be difficult if matching against types as well.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.9 |
| 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":"More lazy orphan module loading","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"7.10.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"ezyang"},"version":"7.9","keywords":["backpack"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Currently, when we import a module, we eagerly load all of the orphan modules transitively reachable from it (TcRnDriver:tcRnImports). This is a bit of bummer: as module import hierarchies get deeper and deeper, we'll collect more and more orphan instances and load more and more modules eagerly.\r\n\r\nThe idea is to try to arrange for an orphan module not to be loaded, unless we think that it might have a relevant instance. Instead of just recording a list of orphan modules transitively reachable from a module, we will also record a digest of what type classes and types the orphan provides instances for. (This will be similar to the data we record for `ifInstTys` in `IfaceClsInst`.)\r\n\r\nNow, when we do any operation involving instances, we check and see if there are also orphans which could provide relevant instances (based on the digest) and load those. If an instance could never have been used, we avoid loading its interface file entirely.\r\n\r\nThis doesn't appear to help too much for type families, where we have to load all of the instances anyway in order to check for consistency.\r\n\r\nA choice to make: Should we record just the class, or also the types involved? It would be best if we could quickly conclude that there are no more instances to load, but this may be difficult if matching against types as well.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Edward Z. YangEdward Z. Yanghttps://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":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/9622GHCi command to solve a constraint2019-07-07T18:39:47ZKrzysztof GogolewskiGHCi command to solve a constraintIt would be nice to have a `:solve` command for ghci that took a class constraint and returned either its derivation or an error message. A possible interface could look like so:
```
ghci> :solve Eq (Maybe Type1, Bool)
1) Eq Type1 ...It would be nice to have a `:solve` command for ghci that took a class constraint and returned either its derivation or an error message. A possible interface could look like so:
```
ghci> :solve Eq (Maybe Type1, Bool)
1) Eq Type1 -- Defined in ‘MyModule’
2) Eq a => Eq (Maybe a) -- Defined in ‘GHC.Classes’
3) Eq (Maybe Type1) -- Put a ~ Int in 2) and use 1)
4) Eq Bool -- Defined in ‘GHC.Classes’
5) (Eq a, Eq b) => Eq (a,b) -- Defined in ‘GHC.Classes’
6) Eq (Maybe Type1, Bool) -- Put a ~ Maybe Type1, b ~ Bool in 5) and use 3), 4)
ghci> :solve Eq (Int -> Int)
No instance for Eq (Int -> Int)
```https://gitlab.haskell.org/ghc/ghc/-/issues/9607Programs that require AllowAmbiguousTypes in 7.82019-07-07T18:39:50ZJan Stolarekjan.stolarek@ed.ac.ukPrograms that require AllowAmbiguousTypes in 7.8Jason McCarty [reported on Haskell-cafe](http://www.haskell.org/pipermail/haskell-cafe/2014-September/116076.html) that this code used to work with GHC 7.6 but in GHC 7.8 it requires `AllowAmbiguousTypes`:
```hs
-- The code below is sim...Jason McCarty [reported on Haskell-cafe](http://www.haskell.org/pipermail/haskell-cafe/2014-September/116076.html) that this code used to work with GHC 7.6 but in GHC 7.8 it requires `AllowAmbiguousTypes`:
```hs
-- The code below is simplified from code that computes a tensor product of
-- a tensor with an identity matrix whose size is determined from the
-- shapes of the input and output tensors.
{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}
--{-# LANGUAGE AllowAmbiguousTypes #-}
module Tensors where
import GHC.TypeLits
type family (as :: [Nat]) ++ (bs :: [Nat]) :: [Nat]
type instance '[] ++ bs = bs
type instance (a ': as) ++ bs = a ': (as ++ bs)
data Tensor (s :: [Nat]) = Tensor -- content elided
-- apparently GHC reduces (++) enough to see that n is determined
leftUnit :: Tensor s -> Tensor ('[n, n] ++ s)
leftUnit Tensor = Tensor
-- accepted in 7.6, not accepted in 7.8 without AllowAmbiguousTypes
rightUnit :: Tensor s -> Tensor (s ++ '[n, n])
rightUnit Tensor = Tensor
-- also accepted without AllowAmbiguousTypes
outsideUnit :: Tensor s -> Tensor ('[n] ++ s ++ '[n])
outsideUnit Tensor = Tensor
useleftUnit :: Tensor '[1,1,2]
useleftUnit = leftUnit Tensor -- type of Tensor is inferred
userightUnit :: Tensor '[1,2,2]
userightUnit = rightUnit (Tensor :: Tensor '[1]) -- type must be provided
```
<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":"Type checking regression between GHC 7.6 and 7.8","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":"Jason McCarty [http://www.haskell.org/pipermail/haskell-cafe/2014-September/116076.html reported on Haskell-cafe] that this code used to work with GHC 7.6 but in GHC 7.8 it requires `AllowAmbiguousTypes`:\r\n\r\n{{{#!hs\r\n-- The code below is simplified from code that computes a tensor product of\r\n-- a tensor with an identity matrix whose size is determined from the\r\n-- shapes of the input and output tensors.\r\n{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}\r\n--{-# LANGUAGE AllowAmbiguousTypes #-}\r\nmodule Tensors where\r\nimport GHC.TypeLits\r\n\r\ntype family (as :: [Nat]) ++ (bs :: [Nat]) :: [Nat]\r\ntype instance '[] ++ bs = bs\r\ntype instance (a ': as) ++ bs = a ': (as ++ bs)\r\n\r\ndata Tensor (s :: [Nat]) = Tensor -- content elided\r\n\r\n-- apparently GHC reduces (++) enough to see that n is determined\r\nleftUnit :: Tensor s -> Tensor ('[n, n] ++ s)\r\nleftUnit Tensor = Tensor\r\n\r\n-- accepted in 7.6, not accepted in 7.8 without AllowAmbiguousTypes\r\nrightUnit :: Tensor s -> Tensor (s ++ '[n, n])\r\nrightUnit Tensor = Tensor\r\n\r\n-- also accepted without AllowAmbiguousTypes\r\noutsideUnit :: Tensor s -> Tensor ('[n] ++ s ++ '[n])\r\noutsideUnit Tensor = Tensor\r\n\r\nuseleftUnit :: Tensor '[1,1,2]\r\nuseleftUnit = leftUnit Tensor -- type of Tensor is inferred\r\n\r\nuserightUnit :: Tensor '[1,2,2]\r\nuserightUnit = rightUnit (Tensor :: Tensor '[1]) -- type must be provided\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/9587Type checking with type functions introduces many type variables, which remai...2019-07-07T18:39:54ZolegType checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks.Before the type ambiguity check was introduced, I could write the following code
```
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- {-# LA...Before the type ambiguity check was introduced, I could write the following code
```
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- {-# LANGUAGE AllowAmbiguousTypes #-}
module T where
type family Arr (repr :: * -> *) (a :: *) (b :: *) :: *
class ESymantics repr where
int :: Int -> repr Int
add :: repr Int -> repr Int -> repr Int
lam :: (repr a -> repr b) -> repr (Arr repr a b)
app :: repr (Arr repr a b) -> repr a -> repr b
{-
te4 :: (Arr repr (Arr repr Int Int) (Arr repr Int Int)
~
Arr repr (Arr repr Int Int) (Arr repr Int b),
ESymantics repr) =>
repr b
-}
te4 = let c3 = lam (\f -> lam (\x -> f `app` (f `app` (f `app` x))))
in (c3 `app` (lam (\x -> x `add` int 14))) `app` (int 0)
-- t = lam (\f -> f `app` int 0)
newtype R a = R{unR :: a}
type instance Arr R a b = a -> b
instance ESymantics R where
int = R
add (R x) (R y) = R $ x + y
lam f = R $ unR . f . R
app (R f) (R x) = R $ f x
tR = unR te4
```
(This is a simple code abstracted from a longer code that for sure worked in 2010: I showed it in a SSGIP lecture at Oxford.) The inferred type of te4
is shown in comments. The type is not ideal but the best what can be done under circumstances. In tR, repr is instantiated to R and the type function Arr can finally be applied and the equality constraint resolved.
Since then, the type inference has changed and the code no longer type checks:
```
Could not deduce (Arr repr (Arr repr a0 b0) (Arr repr a2 b0)
~ Arr repr (Arr repr a b) (Arr repr a4 b))
from the context (ESymantics repr,
Arr repr a4 a3 ~ Arr repr a b,
Arr repr a3 a ~ Arr repr a b)
bound by the inferred type for ‘c3’:
(ESymantics repr, Arr repr a4 a3 ~ Arr repr a b,
Arr repr a3 a ~ Arr repr a b) =>
repr (Arr repr (Arr repr a b) (Arr repr a4 b))
```
What is worse, there does not appear to be \*any\* way to get the code to type check. No amount of type annotations helps. The code has to be dramatically re-written, or just given up.
<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":"Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks.","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":["ambiguity","check","family,","type"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Before the type ambiguity check was introduced, I could write the following code\r\n\r\n{{{\r\n{-# LANGUAGE NoMonomorphismRestriction #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n-- {-# LANGUAGE AllowAmbiguousTypes #-}\r\n\r\nmodule T where\r\n\r\ntype family Arr (repr :: * -> *) (a :: *) (b :: *) :: *\r\n\r\nclass ESymantics repr where\r\n int :: Int -> repr Int\r\n add :: repr Int -> repr Int -> repr Int\r\n\r\n lam :: (repr a -> repr b) -> repr (Arr repr a b)\r\n app :: repr (Arr repr a b) -> repr a -> repr b\r\n\r\n{-\r\nte4 :: (Arr repr (Arr repr Int Int) (Arr repr Int Int)\r\n ~\r\n Arr repr (Arr repr Int Int) (Arr repr Int b),\r\n ESymantics repr) =>\r\n repr b\r\n-}\r\n\r\nte4 = let c3 = lam (\\f -> lam (\\x -> f `app` (f `app` (f `app` x))))\r\n in (c3 `app` (lam (\\x -> x `add` int 14))) `app` (int 0)\r\n\r\n-- t = lam (\\f -> f `app` int 0)\r\n\r\nnewtype R a = R{unR :: a}\r\ntype instance Arr R a b = a -> b\r\n\r\ninstance ESymantics R where\r\n int = R\r\n add (R x) (R y) = R $ x + y\r\n lam f = R $ unR . f . R\r\n app (R f) (R x) = R $ f x\r\n\r\ntR = unR te4\r\n\r\n}}}\r\n\r\n(This is a simple code abstracted from a longer code that for sure worked in 2010: I showed it in a SSGIP lecture at Oxford.) The inferred type of te4\r\nis shown in comments. The type is not ideal but the best what can be done under circumstances. In tR, repr is instantiated to R and the type function Arr can finally be applied and the equality constraint resolved.\r\n\r\nSince then, the type inference has changed and the code no longer type checks:\r\n{{{\r\n\r\nCould not deduce (Arr repr (Arr repr a0 b0) (Arr repr a2 b0)\r\n ~ Arr repr (Arr repr a b) (Arr repr a4 b))\r\n from the context (ESymantics repr,\r\n Arr repr a4 a3 ~ Arr repr a b,\r\n Arr repr a3 a ~ Arr repr a b)\r\n bound by the inferred type for ‘c3’:\r\n (ESymantics repr, Arr repr a4 a3 ~ Arr repr a b,\r\n Arr repr a3 a ~ Arr repr a b) =>\r\n repr (Arr repr (Arr repr a b) (Arr repr a4 b))\r\n}}}\r\n\r\nWhat is worse, there does not appear to be *any* way to get the code to type check. No amount of type annotations helps. The code has to be dramatically re-written, or just given up.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/9522SPECIALISE pragmas for derived instances2023-06-16T08:33:20ZSimon Peyton JonesSPECIALISE pragmas for derived instancesIn package `ghc-prim`, in `GHC.Classes` we have
```
instance (Eq a) => Eq [a] where
{-# SPECIALISE instance Eq [[Char]] #-}
{-# SPECIALISE instance Eq [Char] #-}
{-# SPECIALISE instance Eq [Int] #-}
[] == [] = Tr...In package `ghc-prim`, in `GHC.Classes` we have
```
instance (Eq a) => Eq [a] where
{-# SPECIALISE instance Eq [[Char]] #-}
{-# SPECIALISE instance Eq [Char] #-}
{-# SPECIALISE instance Eq [Int] #-}
[] == [] = True
(x:xs) == (y:ys) = x == y && xs == ys
_xs == _ys = False
```
The `SPECIALISE instance` pragmas instantiate the code for these commonly-used types.
But for tuples we use `deriving`:
```
deriving instance (Eq a, Eq b) => Eq (a, b)
```
and many more similar. There is no way to add a `SPECIALISE instance` pragma for a derived instance. This is bad, because they are heavily used.
You can see the lossage from messages lie
```
WARNING: file compiler/specialise/Specialise.lhs, line 673
specImport discarding:
GHC.Classes.$w$c== :: forall a b. (Eq a, Eq b) => a -> b -> a -> b -> Bool
@ Module.Module @ Module.Module Module.$fEqModule Module.$fEqModule
```
which says that we will end up calling `$w$c==` for pairs of modules, passing dictionaries to compare the modules for equality. These messages show up when compiling the libraries if you build your stage1 compiler with `-DDEBUG`.
It should probably be possible to have a top-level
```
{-# SPECIALISE instance Eq (Int, Bool) #-}
```
even in another module (as we can now do for functions. To do this right, we'd need to make the code for derived methods `INLINEALBE`.https://gitlab.haskell.org/ghc/ghc/-/issues/9518Improve error message for unacceptable role annotations2023-12-06T21:12:16ZdmccleanImprove error message for unacceptable role annotationsIt would be nice if this message:
```
Role mismatch on variable a:
Annotation says representational but role nominal is required
while checking a role annotation for `Point'
```
Could be extended to say where the requirement arises.
...It would be nice if this message:
```
Role mismatch on variable a:
Annotation says representational but role nominal is required
while checking a role annotation for `Point'
```
Could be extended to say where the requirement arises.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 7.8.3 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Improve error message for unacceptable role annotations","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"It would be nice if this message:\r\n\r\n{{{\r\nRole mismatch on variable a:\r\n Annotation says representational but role nominal is required\r\nwhile checking a role annotation for `Point'\r\n}}}\r\n\r\nCould be extended to say where the requirement arises.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/9456Weird behavior with polymorphic function involving existential quantification...2019-07-07T18:40:20ZhaasnWeird behavior with polymorphic function involving existential quantification and GADTsThis program is rejected by GHC 7.8.2:
```
{-# LANGUAGE GADTs, ExistentialQuantification #-}
module Foo where
data Box = forall a. Box a
foo :: Monad m => m ()
foo = do
box <- return (Box ())
let f x =
let _ = Box x `asTy...This program is rejected by GHC 7.8.2:
```
{-# LANGUAGE GADTs, ExistentialQuantification #-}
module Foo where
data Box = forall a. Box a
foo :: Monad m => m ()
foo = do
box <- return (Box ())
let f x =
let _ = Box x `asTypeOf` box
in x
g :: a -> a
g = f
return ()
```
With the following type error:
```
foo.hs:15:11:
Couldn't match type ‘a0’ with ‘a’
because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for g :: a -> a
at foo.hs:14:12-17
Expected type: a -> a
Actual type: a0 -> a0
Relevant bindings include
g :: a -> a (bound at foo.hs:15:7)
f :: a0 -> a0 (bound at foo.hs:10:7)
In the expression: f
In an equation for ‘g’: g = f
```
Perplexingly, however, you can get it to compile either by adding a type signature to f:
```
{-# LANGUAGE GADTs, ExistentialQuantification #-}
module Foo where
data Box = forall a. Box a
foo :: Monad m => m ()
foo = do
box <- return (Box ())
let f :: x -> x
f x =
let _ = Box x `asTypeOf` box
in x
g :: a -> a
g = f
return ()
```
Or by disabling the GADTs extension:
```
{-# LANGUAGE ExistentialQuantification #-}
module Foo where
data Box = forall a. Box a
foo :: Monad m => m ()
foo = do
box <- return (Box ())
let f x =
let _ = Box x `asTypeOf` box
in x
g :: a -> a
g = f
return ()
```
Or by getting rid of the asTypeOf:
```
{-# LANGUAGE GADTs, ExistentialQuantification #-}
module Foo where
data Box = forall a. Box a
foo :: Monad m => m ()
foo = do
box <- return (Box ())
let f x =
let _ = Box x
in x
g :: a -> a
g = f
return ()
```
Or by defining ‘box’ differently:
```
{-# LANGUAGE GADTs, ExistentialQuantification #-}
module Foo where
data Box = forall a. Box a
foo :: Monad m => m ()
foo = do
let box = Box ()
let f x =
let _ = Box x `asTypeOf` box
in x
g :: a -> a
g = f
return ()
```
And perhaps some other factors that I haven't tested yet.
It appears to me that all of these should be valid programs.
Real world source: https://github.com/andygill/io-reactive/blob/master/Control/Concurrent/Reactive.hs
It happens here due to the usage of “writeChan chan $ Req fun ret”, which makes the function requestit in line 77 not as polymorphic as it should be, unless you add a type signature. The putMVar serves the same role as the `asTypeOf` in my smaller example.