type checking failure curiosity

newer
[ANNOUNCE] GHC 9.2.1 now available

Julian Bradfield

14 Nov 2021 14 Nov '21

11:52 a.m.

In the course of updating a tutorial for this year's course, I found the provided code didn't compile. This is because a key value is "undefined" in order for the students to fill it in, but I'm curious why it can't be typechecked nonetheless. The code is: reachable :: (Ord q) => FSM q -> Set(Set(q)) -> Set(Set(q)) reachable fsm@(FSM qs as ts ss fs) supers = let new :: Set(Set(q)) -- typechecking fails without this declaration new = undefined in if null new then supers else reachable fsm (supers \/ new) The \/ in the last line is just Set.union. On the face of it, the last term directly forces "new" to have type Set(Set(q)), so why doesn't Haskell see that? Without the explicit type declaration of "new", we get: • Could not deduce (Foldable t0) arising from a use of ‘null’ from the context: Ord q bound by the type signature for: reachable :: forall q. Ord q => FSM q -> Set (Set q) -> Set (Set q) at CLTutorial9.hs:127:1-60 The type variable ‘t0’ is ambiguous These potential instances exist: instance Foldable (Either a) -- Defined in ‘Data.Foldable’ instance Foldable Set -- Defined in ‘Data.Set.Internal’ instance Foldable Maybe -- Defined in ‘Data.Foldable’ ...plus two others ...plus 27 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the expression: null new In the expression: if null new then supers else reachable fsm (supers \/ new) In the expression: let new = undefined in if null new then supers else reachable fsm (supers \/ new) | 130 | in if null new then supers else reachable fsm (supers \/ new) | ^^^^^^^^

Show replies by date

Brandon Allbery

14 Nov 14 Nov

3:01 p.m.

At a guess, the problem here is that you need to use ScopedTypeVariables and `forall` to bring the right `q` into scope. Otherwise, `q` represents a *new* type variable unrelated to the one in the type signature for `reachable`, and of course ghc cannot reconcile that independent type variable with the requirement that it match the one in the earlier type signature. On Sun, Nov 14, 2021 at 2:58 PM Julian Bradfield wrote:

...

In the course of updating a tutorial for this year's course, I found the provided code didn't compile. This is because a key value is "undefined" in order for the students to fill it in, but I'm curious why it can't be typechecked nonetheless.

The code is:

reachable :: (Ord q) => FSM q -> Set(Set(q)) -> Set(Set(q)) reachable fsm@(FSM qs as ts ss fs) supers = let new :: Set(Set(q)) -- typechecking fails without this declaration new = undefined in if null new then supers else reachable fsm (supers \/ new)

The \/ in the last line is just Set.union.

On the face of it, the last term directly forces "new" to have type Set(Set(q)), so why doesn't Haskell see that?

Without the explicit type declaration of "new", we get:

• Could not deduce (Foldable t0) arising from a use of ‘null’ from the context: Ord q bound by the type signature for: reachable :: forall q. Ord q => FSM q -> Set (Set q) -> Set (Set q) at CLTutorial9.hs:127:1-60 The type variable ‘t0’ is ambiguous These potential instances exist: instance Foldable (Either a) -- Defined in ‘Data.Foldable’ instance Foldable Set -- Defined in ‘Data.Set.Internal’ instance Foldable Maybe -- Defined in ‘Data.Foldable’ ...plus two others ...plus 27 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the expression: null new In the expression: if null new then supers else reachable fsm (supers \/ new) In the expression: let new = undefined in if null new then supers else reachable fsm (supers \/ new) | 130 | in if null new then supers else reachable fsm (supers \/ new) | ^^^^^^^^ _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- brandon s allbery kf8nh allbery.b@gmail.com

Richard Eisenberg

15 Nov 15 Nov

9:25 p.m.

My guess is that you've disabled the monomorphism restriction somehow... but you need the MR to type-check this code. Without the MR, `new` gets a type `forall a. a`, which gets specialized differently in `new`'s two occurrences, meaning that the type information from the second occurrence doesn't affect the first one... which you need it to in order to type-check the `null new` call. I coincidentally ran into this same issue elsewhere today. I think we need to do a better job around error messages in this case. Richard

...

On Nov 14, 2021, at 11:52 AM, Julian Bradfield wrote:

In the course of updating a tutorial for this year's course, I found the provided code didn't compile. This is because a key value is "undefined" in order for the students to fill it in, but I'm curious why it can't be typechecked nonetheless.

The code is:

reachable :: (Ord q) => FSM q -> Set(Set(q)) -> Set(Set(q)) reachable fsm@(FSM qs as ts ss fs) supers = let new :: Set(Set(q)) -- typechecking fails without this declaration new = undefined in if null new then supers else reachable fsm (supers \/ new)

The \/ in the last line is just Set.union.

On the face of it, the last term directly forces "new" to have type Set(Set(q)), so why doesn't Haskell see that?

Without the explicit type declaration of "new", we get:

• Could not deduce (Foldable t0) arising from a use of ‘null’ from the context: Ord q bound by the type signature for: reachable :: forall q. Ord q => FSM q -> Set (Set q) -> Set (Set q) at CLTutorial9.hs:127:1-60 The type variable ‘t0’ is ambiguous These potential instances exist: instance Foldable (Either a) -- Defined in ‘Data.Foldable’ instance Foldable Set -- Defined in ‘Data.Set.Internal’ instance Foldable Maybe -- Defined in ‘Data.Foldable’ ...plus two others ...plus 27 instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the expression: null new In the expression: if null new then supers else reachable fsm (supers \/ new) In the expression: let new = undefined in if null new then supers else reachable fsm (supers \/ new) | 130 | in if null new then supers else reachable fsm (supers \/ new) | ^^^^^^^^ _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Julian Bradfield

16 Nov 16 Nov

7:44 a.m.

...

My guess is that you've disabled the monomorphism restriction somehow... but you need the MR to type-check this code. Without the MR, `new` gets a type `forall a. a`, which gets specialized differently in `new`'s two occurrences, meaning that the type information from the second occurrence doesn't affect the first one... which you need it to in order to type-check the `null new` call.

Hm. I see the MR is off at the command prompt by default, but on in compiled modules. The offending code was in a module starting: module CLTutorial9 where import Prelude hiding (lookup) import Data.Set(Set, insert, empty, member, fromList, toList, union,intersection, size, singleton, (\\)) import qualified Data.Set as S import Test.QuickCheck import Data.Char I haven't knowingly done any thing to turn off the MR.

Richard Eisenberg

11:26 a.m.

Perhaps you're right -- the monomorphism restriction wouldn't fire there, because there's no constraint to monomorphise. Instead, you just want a monomorphic `new`.... but I see no easy way (other than a type signature) to get this. Think of it this way: without the type annotation, you've said `let new = undefined in ...`. Now, replace `new` with `undefined` everywhere you've written `new`. Your code will include `null undefined`, which is indeed irresolvably ambiguous. Richard

...

On Nov 16, 2021, at 7:44 AM, Julian Bradfield wrote:

...
My guess is that you've disabled the monomorphism restriction somehow... but you need the MR to type-check this code. Without the MR, `new` gets a type `forall a. a`, which gets specialized differently in `new`'s two occurrences, meaning that the type information from the second occurrence doesn't affect the first one... which you need it to in order to type-check the `null new` call.

Hm. I see the MR is off at the command prompt by default, but on in compiled modules. The offending code was in a module starting:

module CLTutorial9 where import Prelude hiding (lookup) import Data.Set(Set, insert, empty, member, fromList, toList, union,intersection, size, singleton, (\\)) import qualified Data.Set as S import Test.QuickCheck import Data.Char

I haven't knowingly done any thing to turn off the MR.

J. Garrett Morris

17 Nov 17 Nov

10:27 p.m.

I suspect that if `null` still had type `[t] -> Bool`, Julian's code would compile. /g On Tue, Nov 16, 2021 at 10:27 AM Richard Eisenberg wrote:

...

Perhaps you're right -- the monomorphism restriction wouldn't fire there, because there's no constraint to monomorphise. Instead, you just want a monomorphic `new`.... but I see no easy way (other than a type signature) to get this.

Think of it this way: without the type annotation, you've said `let new = undefined in ...`. Now, replace `new` with `undefined` everywhere you've written `new`. Your code will include `null undefined`, which is indeed irresolvably ambiguous.

Richard

...
On Nov 16, 2021, at 7:44 AM, Julian Bradfield < jcb+hc@julianbradfield.org> wrote:

...
My guess is that you've disabled the monomorphism restriction somehow... but you need the MR to type-check this code. Without the MR, `new` gets a type `forall a. a`, which gets specialized differently in `new`'s two occurrences, meaning that the type information from the second occurrence doesn't affect the first one... which you need it to in order to type-check the `null new` call.

Hm. I see the MR is off at the command prompt by default, but on in compiled modules. The offending code was in a module starting:

module CLTutorial9 where import Prelude hiding (lookup) import Data.Set(Set, insert, empty, member, fromList, toList, union,intersection, size, singleton, (\\)) import qualified Data.Set as S import Test.QuickCheck import Data.Char

I haven't knowingly done any thing to turn off the MR.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- Prosperum ac felix scelus virtus vocatur -- Seneca

1397

Age (days ago)

1401

Last active (days ago)

List overview

Download

5 comments

4 participants

participants (4)

Brandon Allbery
J. Garrett Morris
Julian Bradfield
Richard Eisenberg