Opened 3 years ago

Closed 3 years ago

Last modified 3 years ago

#8450 closed feature request (fixed)

can't match type Bool with (), but shouldn't have to

Reported by: dmwit Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.6.3
Keywords: Cc: dimitris@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T8450
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


The following (definitely type-incorrect) file:

{-# LANGUAGE ScopedTypeVariables #-}

runEffect :: Either Bool r -> r
runEffect = undefined

run :: forall a. a
run = runEffect $ (undefined :: Either a ())

produces the following error:

    Couldn't match type `Bool' with `()'
    Expected type: a
      Actual type: ()
    In the expression: runEffect $ (undefined :: Either a ())
    In an equation for `run':
        run = runEffect $ (undefined :: Either a ())

This is strange because one of the two types it claims it can't unify (Bool) doesn't appear in either the expected or actual type. Note that removing the ($) gets a different error message that makes it a bit more clear what's going on:

    Couldn't match type `Bool' with `()'
    Expected type: Either Bool a
      Actual type: Either a ()
    In the first argument of `runEffect', namely
      `(undefined :: Either a ())'
    In the expression: runEffect (undefined :: Either a ())
    In an equation for `run':
        run = runEffect (undefined :: Either a ())

So it seems it's trying to unify Bool and () because it's unifying both a with Bool and a with (); however, the usual comments about rigid type variables aren't there, which makes even this error message a bit confusing.

Change History (5)

comment:1 Changed 3 years ago by carter

I hit this problem or something very very close to it, earlier this week. Though in my case it was for type correct code that i had to hoist out as a top level definition to type check.. I'll see if i can repro it in a smaller example.

comment:2 Changed 3 years ago by simonpj

Cc: dimitris@… added

Nice example. (The rest of this is cryptic comments mainly for Dimitrios.)

The issue is this. We have a skolem 'a', and two constraints

	[w} a ~ Bool
	[w] a ~ ()

But because we rewrite wanteds with wanteds, we rewrite to

	[w] Bool ~ ()

which is really quite unhelpful.

I'm beginning to wonder: what would happen if we never rewrote a wanted with another wanted?

comment:3 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 06aac68dee100b21dc7d304fa90d9baa423507a0/ghc:

Refactor the constraint solver (again!)

There are three core changes here:

a) In the constraint-solver pipeline.
   Given a work-item 'wi', the old scheme was:
      let relevant = getRelevantInerts wi
      interact 'wi' with each constraint in 'relevant'
   Bu now we have a single step
      interact 'wi' with the inert-set

   This turns out to avoid duplication, between getRelevantInerts
   (which needs to know which are relevant) and the interact step.
   Simpler, cleaner.

   This in turn made it sensible to combine the 'spontaneous solve'
   stage into the 'interact with inerts' stage.

b) Wanteds are no longer used to rewrite wanteds.  See Trac #8450.
   This in turn means that the inert set may have
     - many CFunEqCans with the same LHS
     - many CTyEqCans  with the same LHS
   Hence the EqualCtList in teh domain of inert_eqs and inert_funeqs

c) Some refactoring of the representation of the inert set,
   Notably inert_dicts and inert_funeqs are indexed by Class and TyCon
   respectively, so we can easily get all the constraints relevant to
   that class or tycon

There are many knock on effects!  This started as a small job but I
ended up doing qite a lot.  Some error messages in the test suite
really did improve as a result of (b)

comment:4 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

comment:5 Changed 3 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/T8450

Thank you for the provocation. Things are much better now.


Note: See TracTickets for help on using tickets.