GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2021-09-15T13:05:09Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/8388forall on non-* types2021-09-15T13:05:09ZKrzysztof Gogolewskiforall on non-* typesThis code
```
{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}
x = Nothing :: (forall a. Maybe) Int
```
gives
```
Couldn't match type `Maybe' with `forall a. Maybe'
Expected type: forall a. Maybe Int
Actual type: Maybe In...This code
```
{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}
x = Nothing :: (forall a. Maybe) Int
```
gives
```
Couldn't match type `Maybe' with `forall a. Maybe'
Expected type: forall a. Maybe Int
Actual type: Maybe Int
```
which does not seem correct. There are two options:
Option A: We allow this.
Option B: We reject this as ill-kinded and allow `forall a. T` only when `T` has kind `*`. I prefer this option; in theory this can break existing code, but I am not aware of any code that uses forall on non-\* type (please correct me if I'm wrong), and e.g. this means `forall a. a` inhabits every kind, for example `Bool`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"forall on non-* types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code\r\n\r\n{{{\r\n{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}\r\nx = Nothing :: (forall a. Maybe) Int\r\n}}}\r\n\r\ngives\r\n\r\n{{{\r\n Couldn't match type `Maybe' with `forall a. Maybe'\r\n Expected type: forall a. Maybe Int\r\n Actual type: Maybe Int\r\n}}}\r\n\r\nwhich does not seem correct. There are two options:\r\n\r\nOption A: We allow this.\r\n\r\nOption B: We reject this as ill-kinded and allow `forall a. T` only when `T` has kind `*`. I prefer this option; in theory this can break existing code, but I am not aware of any code that uses forall on non-* type (please correct me if I'm wrong), and e.g. this means `forall a. a` inhabits every kind, for example `Bool`.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/7870Compilation errors break the complexity encapsulation on DSLs, impairs succ...2019-07-07T18:47:44ZagocoronaCompilation errors break the complexity encapsulation on DSLs, impairs success in industryFrom the paper "Scripting the Type Inference Process" -Bastiaan Heeren Jurriaan Hage S. Doaitse Swierstra:
1. .. Combinator languages are a means of deﬁning domain speciﬁc languages embedded within an existing programming language, usin...From the paper "Scripting the Type Inference Process" -Bastiaan Heeren Jurriaan Hage S. Doaitse Swierstra:
1. .. Combinator languages are a means of deﬁning domain speciﬁc languages embedded within an existing programming language, using the abstraction facilities present in the latter. However, since the domain speciﬁc extensions are mapped to constructs present in the underlying language, all type errors are reported in terms of the host language, and not in terms of concepts from the combinator library. In addition, the developer of a combinator library may be aware of various mistakes which users of the library can make, something which he can explain in the documentation for the library, but which he cannot make part of the library itself.
1. ..As a result, the beginning programmer is likely to be discouraged from pro-gramming in a functional language, and may see the rejection of programs as a nuisance instead of a blessing. The experienced user might not look at the messages at all.
Definitively this is probably the biggest barrier for the acceptance of Haskell on Industry. We need to start with something not as sophisticated as the Helium paper "Scripting the Type Inference Process", but maybe a partial implementation of the techniques mentioned, so that the development can be enhanced in the future.
Maybe some kind of library that permits postprocessing of GHC errors and/or the identification of points in the current type checker where some kind of rules can be defined by the programmer can be the first step.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.7 |
| 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":"Compilation errors break the complexity encapsulation on DSLs, impairs success in industry","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":["DSL,","Error,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"From the paper \"Scripting the Type Inference Process\" -Bastiaan Heeren Jurriaan Hage S. Doaitse Swierstra:\r\n\r\n\r\n... Combinator languages are a means of deﬁning domain speciﬁc languages embedded within an existing programming language, using the abstraction facilities present in the latter. However, since the domain speciﬁc extensions are mapped to constructs present in the underlying language, all type errors are reported in terms of the host language, and not in terms of concepts from the combinator library. In addition, the developer of a combinator library may be aware of various mistakes which users of the library can make, something which he can explain in the documentation for the library, but which he cannot make part of the library itself.\r\n\r\n...As a result, the beginning programmer is likely to be discouraged from pro-gramming in a functional language, and may see the rejection of programs as a nuisance instead of a blessing. The experienced user might not look at the messages at all.\r\n\r\nDefinitively this is probably the biggest barrier for the acceptance of Haskell on Industry. We need to start with something not as sophisticated as the Helium paper \"Scripting the Type Inference Process\", but maybe a partial implementation of the techniques mentioned, so that the development can be enhanced in the future. \r\n\r\nMaybe some kind of library that permits postprocessing of GHC errors and/or the identification of points in the current type checker where some kind of rules can be defined by the programmer can be the first step. ","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/7842Incorrect checking of let-bindings in recursive do2019-07-07T18:47:51ZIavor S. DiatchkiIncorrect checking of let-bindings in recursive doI have run into a problem with the type-checking of recursive do blocks, which reduces to the following example:
```
{-# LANGUAGE RecursiveDo #-}
module Bug where
bug :: (Int -> IO Int) -> IO (Bool, Char)
bug m =
mdo i <- m i1 -...I have run into a problem with the type-checking of recursive do blocks, which reduces to the following example:
```
{-# LANGUAGE RecursiveDo #-}
module Bug where
bug :: (Int -> IO Int) -> IO (Bool, Char)
bug m =
mdo i <- m i1 -- RECURSION
let i1 :: Int
i1 = i -- RECURSION
-- This appears to be monomorphic, despite the type signature.
f :: b -> b
f x = x
return (f True, f 'a')
```
This program is rejected with the errors shown below. The problem appears to be that somehow `f` has become monomorphic, despite its type-signature. This seems to happen only when `f` is part of a `let` block that is also involved in the recursion.
Here is the error reported by GHC 7.7.20130215:
```
Bug.hs:15:23:
Couldn't match expected type `Char' with actual type `Bool'
In the return type of a call of `f'
In the expression: f 'a'
In the first argument of `return', namely `(f True, f 'a')'
Bug.hs:15:25:
Couldn't match expected type `Bool' with actual type `Char'
In the first argument of `f', namely 'a'
In the expression: f 'a'
In the first argument of `return', namely `(f True, f 'a')'
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.7 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Incorrect checking of let-bindings in recursive do","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.7","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I have run into a problem with the type-checking of recursive do blocks, which reduces to the following example:\r\n\r\n{{{\r\n{-# LANGUAGE RecursiveDo #-}\r\nmodule Bug where\r\n\r\nbug :: (Int -> IO Int) -> IO (Bool, Char)\r\nbug m =\r\n mdo i <- m i1 -- RECURSION\r\n\r\n let i1 :: Int\r\n i1 = i -- RECURSION\r\n\r\n -- This appears to be monomorphic, despite the type signature.\r\n f :: b -> b\r\n f x = x\r\n\r\n return (f True, f 'a')\r\n}}}\r\n\r\nThis program is rejected with the errors shown below. The problem appears to be that somehow `f` has become monomorphic, despite its type-signature. This seems to happen only when `f` is part of a `let` block that is also involved in the recursion.\r\n\r\nHere is the error reported by GHC 7.7.20130215:\r\n\r\n{{{\r\nBug.hs:15:23:\r\n Couldn't match expected type `Char' with actual type `Bool'\r\n In the return type of a call of `f'\r\n In the expression: f 'a'\r\n In the first argument of `return', namely `(f True, f 'a')'\r\n\r\nBug.hs:15:25:\r\n Couldn't match expected type `Bool' with actual type `Char'\r\n In the first argument of `f', namely 'a'\r\n In the expression: f 'a'\r\n In the first argument of `return', namely `(f True, f 'a')'\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/6065Suggested type signature causes a type error (even though it appears correct)2019-07-07T18:52:21ZtvynrSuggested type signature causes a type error (even though it appears correct)The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon OverlappingInstances and so forth). The definition of the upcast ...The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon OverlappingInstances and so forth). The definition of the upcast function appears to be correct. Compiling without a type signature produces a warning and the suggestion to include a type signature. Including the suggested type signature (which appears to be the correct one) causes a type error.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------------------- |
| Version | 7.4.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | zep_haskell_trac@bahj.com |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Suggested type signature causes a type error (even though it appears correct)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.4.1","keywords":["forall","instance","signature","type","typeclass"],"differentials":[],"test_case":"","architecture":"","cc":["zep_haskell_trac@bahj.com"],"type":"Bug","description":"The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon OverlappingInstances and so forth). The definition of the upcast function appears to be correct. Compiling without a type signature produces a warning and the suggestion to include a type signature. Including the suggested type signature (which appears to be the correct one) causes a type error.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/4894Missing improvement for fun. deps.2019-07-07T18:58:01ZIavor S. DiatchkiMissing improvement for fun. deps.The problem is illustrated by the following example:
```
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
class F a b | a -> b
f :: (F a b, F a c) => a -> b -> c
f _ = id
Results in the following error:
Could not d...The problem is illustrated by the following example:
```
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
class F a b | a -> b
f :: (F a b, F a c) => a -> b -> c
f _ = id
Results in the following error:
Could not deduce (b ~ c)
from the context (F a b, F a c)
bound by the type signature for f :: (F a b, F a c) => a -> b -> c
at bug.hs:6:1-8
`b' is a rigid type variable bound by
the type signature for f :: (F a b, F a c) => a -> b -> c
at bug.hs:6:1
`c' is a rigid type variable bound by
the type signature for f :: (F a b, F a c) => a -> b -> c
at bug.hs:6:1
Expected type: b -> c
Actual type: b -> b
In the expression: id
In an equation for `f': f _ = id
```
The issue seems to be related to Note \[When improvement happens\] in module TcInteract. It states that two "givens" do not interact for the purposes of improvement.
As far as I understand, the correct behavior should be to generate a new given equality, justified by the functional dependency on the class.
This is also related to bug #1241: in order to justify an improvement by functional dependency, we have to check that all instances are consistent with the dependency. Otherwise, the above function would turn into an "unsafe cast" function.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 7.1 |
| 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":"Missing improvement for fun. deps.","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The problem is illustrated by the following example:\r\n\r\n{{{\r\n{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}\r\n\r\nclass F a b | a -> b\r\n\r\nf :: (F a b, F a c) => a -> b -> c\r\nf _ = id\r\n\r\nResults in the following error:\r\n\r\n Could not deduce (b ~ c)\r\n from the context (F a b, F a c)\r\n bound by the type signature for f :: (F a b, F a c) => a -> b -> c\r\n at bug.hs:6:1-8\r\n `b' is a rigid type variable bound by\r\n the type signature for f :: (F a b, F a c) => a -> b -> c\r\n at bug.hs:6:1\r\n `c' is a rigid type variable bound by\r\n the type signature for f :: (F a b, F a c) => a -> b -> c\r\n at bug.hs:6:1\r\n Expected type: b -> c\r\n Actual type: b -> b\r\n In the expression: id\r\n In an equation for `f': f _ = id\r\n}}}\r\n\r\nThe issue seems to be related to Note [When improvement happens] in module TcInteract. It states that two \"givens\" do not interact for the purposes of improvement.\r\n\r\nAs far as I understand, the correct behavior should be to generate a new given equality, justified by the functional dependency on the class.\r\n\r\nThis is also related to bug #1241: in order to justify an improvement by functional dependency, we have to check that all instances are consistent with the dependency. Otherwise, the above function would turn into an \"unsafe cast\" function.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/1928Confusing type error message2019-07-07T19:11:00ZjosefConfusing type error messageThe following code (which is part of a bigger module) needs scoped type variables to compile.
```
run_state :: forall a s. State s a -> s -> (a,s)
run_state m s = observe_monad unit_op bind_op m where
unit_op v = (v,s)
bind...The following code (which is part of a bigger module) needs scoped type variables to compile.
```
run_state :: forall a s. State s a -> s -> (a,s)
run_state m s = observe_monad unit_op bind_op m where
unit_op v = (v,s)
bind_op :: BindOp (StateE s) a (a,s)
bind_op Get k = run_state (k s) s
bind_op (Put s1) k = run_state (k ()) s1
```
However, forgetting to turn on scoped type variables will give a very confusing error message:
```
Unimo.hs:56:36:
Couldn't match expected type `s1' against inferred type `s'
`s1' is a rigid type variable bound by
the type signature for `bind_op' at Unimo.hs:55:28
`s' is a rigid type variable bound by
the type signature for `run_state' at Unimo.hs:52:22
In the first argument of `k', namely `s'
In the first argument of `run_state', namely `(k s)'
In the expression: run_state (k s) s
```
Line 52 is the type signature of run_state and line 55 is the type signature of bind_op. The error message talks about a type variable \`s1' which isn't mentioned anywhere. I guess the reason for this is that we have name collision and this is ghc's way of trying to tell the two variables apart. I don't think it works that well though. But I'm afraid I don't have any suggestion on how to make it better.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | Unknown |
| Architecture | Unknown |
</details>
<!-- {"blocked_by":[],"summary":"Confusing type error message","status":"New","operating_system":"Unknown","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.8.1","keywords":[],"differentials":[],"test_case":"","architecture":"Unknown","cc":[""],"type":"Bug","description":"The following code (which is part of a bigger module) needs scoped type variables to compile.\r\n\r\n{{{\r\nrun_state :: forall a s. State s a -> s -> (a,s)\r\nrun_state m s = observe_monad unit_op bind_op m where\r\n unit_op v = (v,s)\r\n bind_op :: BindOp (StateE s) a (a,s)\r\n bind_op Get k = run_state (k s) s\r\n bind_op (Put s1) k = run_state (k ()) s1\r\n}}}\r\nHowever, forgetting to turn on scoped type variables will give a very confusing error message:\r\n{{{\r\nUnimo.hs:56:36:\r\n Couldn't match expected type `s1' against inferred type `s'\r\n `s1' is a rigid type variable bound by\r\n the type signature for `bind_op' at Unimo.hs:55:28\r\n `s' is a rigid type variable bound by\r\n the type signature for `run_state' at Unimo.hs:52:22\r\n In the first argument of `k', namely `s'\r\n In the first argument of `run_state', namely `(k s)'\r\n In the expression: run_state (k s) s\r\n}}}\r\nLine 52 is the type signature of run_state and line 55 is the type signature of bind_op. The error message talks about a type variable `s1' which isn't mentioned anywhere. I guess the reason for this is that we have name collision and this is ghc's way of trying to tell the two variables apart. I don't think it works that well though. But I'm afraid I don't have any suggestion on how to make it better.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/1614Type checker does not use functional dependency to avoid ambiguity2019-07-07T19:12:36ZguestType checker does not use functional dependency to avoid ambiguityCompiling the following module gives an error
```
module X where
class C a | -> a
instance C Int
unC :: (C a) => a -> Int
unC i = undefined
test :: Int
test = unC undefined
```
Error message:
```
X.hs:13:7:
Ambiguous type varia...Compiling the following module gives an error
```
module X where
class C a | -> a
instance C Int
unC :: (C a) => a -> Int
unC i = undefined
test :: Int
test = unC undefined
```
Error message:
```
X.hs:13:7:
Ambiguous type variable `a' in the constraint:
`C a' arising from a use of `unC' at X.hs:13:7-19
Probable fix: add a type signature that fixes these type variable(s)
```
But that is just plain wrong. The functional dependency in the definition of C forces a to be Int. No other type is possible. So what's ambiguous about that?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 6.7 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | lennart@augustsson.net |
| Operating system | MacOS X |
| Architecture | x86 |
</details>
<!-- {"blocked_by":[],"summary":"Type checker does not use fundep to avoid ambiguity","status":"New","operating_system":"MacOS X","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.7","keywords":[],"differentials":[],"test_case":"","architecture":"x86","cc":["lennart@augustsson.net"],"type":"Bug","description":"Compiling the following module gives an error\r\n{{{\r\nmodule X where\r\n\r\nclass C a | -> a\r\ninstance C Int\r\n\r\nunC :: (C a) => a -> Int\r\nunC i = undefined\r\n\r\ntest :: Int\r\ntest = unC undefined\r\n}}}\r\nError message:\r\n{{{\r\nX.hs:13:7:\r\n Ambiguous type variable `a' in the constraint:\r\n `C a' arising from a use of `unC' at X.hs:13:7-19\r\n Probable fix: add a type signature that fixes these type variable(s)\r\n}}}\r\n\r\nBut that is just plain wrong. The functional dependency in the definition of C forces a to be Int. No other type is possible. So what's ambiguous about that?","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/1451Provide way to show the origin of a constraint2019-07-07T19:13:30Ziampure@gmail.comProvide way to show the origin of a constraintFor a complex type (A b, C d, E e) =\> Something a b e -\> Int, provide a way to given the query:
where does A b come from? Respond with the line number of a function that causes that constraint. This should of course also work for non-H...For a complex type (A b, C d, E e) =\> Something a b e -\> Int, provide a way to given the query:
where does A b come from? Respond with the line number of a function that causes that constraint. This should of course also work for non-Haskell 98 constraints.
This issue comes up when one by accident calls a function in the wrong layer of a monadic transformer stack.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 6.6.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | Unknown |
| Architecture | Unknown |
</details>
<!-- {"blocked_by":[],"summary":"Provide way to show the origin of a constraint","status":"New","operating_system":"Unknown","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"6.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"Unknown","cc":[""],"type":"FeatureRequest","description":"For a complex type (A b, C d, E e) => Something a b e -> Int, provide a way to given the query:\r\nwhere does A b come from? Respond with the line number of a function that causes that constraint. This should of course also work for non-Haskell 98 constraints. \r\n\r\nThis issue comes up when one by accident calls a function in the wrong layer of a monadic transformer stack.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/1158Problem with GADTs and explicit type signatures2019-07-07T19:15:02ZguestProblem with GADTs and explicit type signatures```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Main where
data Exp a where
Val :: a -> Exp b
App :: Exp a -> Exp b
instance Sh...```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Main where
data Exp a where
Val :: a -> Exp b
App :: Exp a -> Exp b
instance Show (Exp a) where
show (Val _) = "Val"
show (App _) = "App"
class LiftToExp a b where
liftToExp :: a -> Exp b
instance LiftToExp (Exp a) a where
liftToExp = id
instance Floating a => LiftToExp a b where
liftToExp v = Val v :: Exp b
{-
Uncommenting the type signature below causes GHCi to fail to load the file:
Test.hs:48:15: error:
• Overlapping instances for LiftToExp a a0
arising from a use of ‘liftToExp’
Matching givens (or their superclasses):
LiftToExp a a1
bound by the type signature for:
test :: LiftToExp a a1 => a -> Exp b
at Test.hs:47:1-38
Matching instances:
instance LiftToExp a b -- Defined at Test.hs:22:10
instance LiftToExp (Exp a) a -- Defined at Test.hs:19:10
(The choice depends on the instantiation of ‘a, a0’)
• In the first argument of ‘App’, namely ‘(liftToExp x)’
In the expression: App (liftToExp x)
In an equation for ‘test’: test x = App (liftToExp x)
However typing :t test at the GHCi prompt gives this exact signature.
-}
--test :: (LiftToExp a a1) => a -> Exp b
test x = App (liftToExp x)
main = putStrLn $ show (test (3.0::Float)::Exp Int)
```Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/816Weird fundep behavior (with -fallow-undecidable-instances)2020-11-24T19:00:53ZnibroWeird fundep behavior (with -fallow-undecidable-instances)I encounter a strange behavior with functional dependencies. Consider this program
```
class Foo x y | x -> y where
foo :: x -> y
class Bar x y where
bar :: x -> y -> Int
instance (Foo x y, Bar y z) => Bar x z where
bar x z = bar (...I encounter a strange behavior with functional dependencies. Consider this program
```
class Foo x y | x -> y where
foo :: x -> y
class Bar x y where
bar :: x -> y -> Int
instance (Foo x y, Bar y z) => Bar x z where
bar x z = bar (foo x) z
```
Compiling (with 6.4.2, -fallow-undecidable-instances and -fglasgow-exts) I get the following error message:
```
Foo.hs:12:0:
Context reduction stack overflow; size = 21
Use -fcontext-stack20 to increase stack size to (e.g.) 20
`$dBar :: Bar y z' arising from use of `bar' at Foo.hs:13:11-13
[... same thing 20 times ...]
`$dBar :: Bar y z' arising from use of `bar' at Foo.hs:13:11-13
`bar :: {bar at [y z]}' arising from use of `bar' at Foo.hs:13:11-13
When trying to generalise the type inferred for `bar'
Signature type: forall x y z. (Foo x y, Bar y z) => x -> z -> Int
Type to generalise: x -> z -> Int
In the instance declaration for `Bar x z'
```
The declaration requires undecidable instances, but I doubt that the problem comes from that. What makes it even more weird is that I can get this to compile, and behave as expected, if I do one of a) declare an instance of Bar for any type, or
b) add an explicit type signature (foo x :: y) in the definition of Bar. The first seems weird since how could a different, unrelated instance affect the typeability of the second instance? The second, b), is weird since by the FD x -\> y we should already know that foo x :: y.
Same behavior in GHC 6.4.1. Hugs (with -98 +O) accepts the code.https://gitlab.haskell.org/ghc/ghc/-/issues/589Various poor type error messages2019-07-07T19:17:44ZPeter A Jonsson [pj@ludd.ltu.se]Various poor type error messagesHello,
I read the summary of the survey and noticed you wanted feedback on
where error messages could be improved. I looked up some (simple)
examples of type errors and ran them through ghc. I do not make any
claims to be an HCI expert,...Hello,
I read the summary of the survey and noticed you wanted feedback on
where error messages could be improved. I looked up some (simple)
examples of type errors and ran them through ghc. I do not make any
claims to be an HCI expert, just a mere mortal with an opinion.
**Type error 1**
Code:
```
module Test2 where
fib n = if (3 > n) then 1 else (fib (n - 1) + fib (n - 2))
k = fib 's'
```
Error message:
```
Test2.hs:4:
No instance for (Num Char)
arising from use of `fib' at Test2.hs:4
In the definition of `k': k = fib 's'
```
This isn't a bad error message in my humble opinion, it does pinpoint
that I'm doing something wrong in line 4, and that there isn't an
instance for Num Char doesn't come as a surprise. However I think it
could have been more helpful by telling me that I tried to pass a Char
to a function which expected an (Ord a, Num a) =\> a as its parameter.
**Type error 2**
Code:
```
module Test4 where
k :: Int -> Int
k l = 2.0*l
```
Error message:
```
Test4.hs:4:
No instance for (Fractional Int)
arising from the literal `2.0' at Test4.hs:4
In the first argument of `(*)', namely `2.0'
In the definition of `k': k l = 2.0 * l
```
One reason this kind of error could happen is an inexperienced user
declaring the wrong type for his function, or not knowing that 2.0
would be interpreted as a Fractional.
**Type error 3**
Code:
```
module Test7 where
len' xs = head (xs) + (length xs)
o = len' "GH"
```
Error message:
```
Test7.hs:4:
Couldn't match `Int' against `Char'
Expected type: [Int]
Inferred type: [Char]
In the first argument of `len'', namely `"GH"'
In the definition of `o': o = len' "GH"
```
I ran this through Hugs version November 2002 and got this error
message:
```
ERROR "Test7.hs":4 - Type error in application
*** Expression : len' "GH"
*** Term : "GH"
*** Type : String
*** Does not match : [Int]
```
I find the Hugs message more clear, but that might be my background.
**Type error 4**
Code:
```
module Test8 where
f = head 3
```
Error message:
```
Test8.hs:3:
No instance for (Num [a])
arising from the literal `3' at Test8.hs:3
Possible cause: the monomorphism restriction applied to the following:
f :: a (bound at Test8.hs:3)
Probable fix: give these definition(s) an explicit type signature
In the first argument of `head', namely `3'
In the definition of `f': f = head 3
```
This one I find outright scary. For "wrong = div 3 8 + 1/2" it gives
an error message that somewhat helps me guess the error, but the above
doesn't even come close to helping me.
/ Peterhttps://gitlab.haskell.org/ghc/ghc/-/issues/472Supertyping of classes2019-07-07T19:17:50ZnobodySupertyping of classessee
[Supertyping Suggestion for Haskell](http://repetae.net/john/recent/out/supertyping.html)
example:
```
class Num a <= Group a where
(+) :: a -> a -> a
negate :: a -> a
```
apart from multiple inheritance, it could work like thi...see
[Supertyping Suggestion for Haskell](http://repetae.net/john/recent/out/supertyping.html)
example:
```
class Num a <= Group a where
(+) :: a -> a -> a
negate :: a -> a
```
apart from multiple inheritance, it could work like this:
```
import Prelude hiding ((+),negate)
import qualified Prelude ((+),negate)
class Group a where
(+) :: a -> a -> a
negate :: a -> a
instance Num a => Group a where
(+) = (Prelude.+)
negate = Prelude.negate
```
- coeus_at_gmx_dehttps://gitlab.haskell.org/ghc/ghc/-/issues/393functions without implementations2019-07-07T19:18:11ZGhost Userfunctions without implementations```
Allow to declare a function by only supplying its type
signature.
This feature shall enhance rapid prototyping by fixing
an interface but leaving some functions unimplemented.
Currently this can be (only) simulated by supplying
dumm...```
Allow to declare a function by only supplying its type
signature.
This feature shall enhance rapid prototyping by fixing
an interface but leaving some functions unimplemented.
Currently this can be (only) simulated by supplying
dummy implementations, like
f :: ...
f = undefined
Since it is possible to supply dummy data types by
"data T" (not followed by "="), allowing functions
without implementations seems almost to be a logical
consequence. Surely, the compiler should emit warnings
for missing implementations.
It would be nice if such function declarations via type
signatures could be repeated at any position within a
module.
```IcelandjackIcelandjackhttps://gitlab.haskell.org/ghc/ghc/-/issues/345GADT - fundep interaction2019-07-07T19:18:23ZbringGADT - fundep interaction```
GADTs and fundeps don't seem to interact in the way
that I (perhaps naively) expect. I expected that for
each case, the type variables would be instantiated
according to the type of the constructors, and then the
fundep would be used...```
GADTs and fundeps don't seem to interact in the way
that I (perhaps naively) expect. I expected that for
each case, the type variables would be instantiated
according to the type of the constructors, and then the
fundep would be used to figure out the result type.
{-# OPTIONS_GHC -fglasgow-exts #-}
data Succ n
data Zero
class Plus x y z | x y -> z
instance Plus Zero x x
instance Plus x y z => Plus (Succ x) y (Succ z)
infixr 5 :::
data List :: * -> * -> * where
Nil :: List a Zero
(:::) :: a -> List a n -> List a (Succ n)
append :: Plus x y z => List a x -> List a y -> List a z
append Nil ys = ys
append (x ::: xs) ys = x ::: append xs ys
{-
GHC 6.4 says:
Couldn't match the rigid variable `y' against `Succ z'
`y' is bound by the type signature for `append'
Expected type: List a y
Inferred type: List a (Succ z)
In the expression: x ::: (append xs ys)
In the definition of `append': append (x ::: xs) ys
= x ::: (append xs ys)
-}
```Simon Peyton JonesSimon Peyton Jones