Opened 3 years ago

Closed 2 years ago

#13530 closed bug (fixed)

Horrible error message due to TypeInType

Reported by: simonpj Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T13530
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

Consider this

{-# LANGUAGE MagicHash, UnboxedTuples #-}

module Foo where

import GHC.Exts

g :: Int -> (# Int#, a #)
g (I# y) = (# y, undefined #)

f :: Int -> (# Int#, Int# #)
f x = g x

With GHC 8 we get

Foo.hs:11:7: error:
    • Couldn't match a lifted type with an unlifted type
      Expected type: (# Int#, Int# #)
        Actual type: (# Int#, Int# #)

What a terrible error message!! It was much better in GHC 7.10:

    Couldn't match kind ‘*’ with ‘#’
    When matching types
      a0 :: *
      Int# :: #
    Expected type: (# Int#, Int# #)
      Actual type: (# Int#, a0 #)

What's going on?

The constraint solver sees

[W] alpha::TYPE LiftedRep  ~  Int#::TYPE IntRep

So it homogenises the kinds, and unifies alpha (this did not happen in GHC 7.10), thus

alpha := Int# |> TYPE co

[W] co :: LiftedRep ~ IntRep

Of course the new constraint fails. But since we have unified alpha, when we print out the types are are unifying they both look like (# Int#, Int# #) (there's a suppressed cast in the second component).

I'm not sure what to do here.

(I tripped over this when debugging #13509.)

Change History (7)

comment:1 Changed 3 years ago by simonpj

Keywords: TypeInType added

comment:2 Changed 3 years ago by goldfire

I think this is #11198.

comment:3 Changed 3 years ago by simonpj

Dead right. We should fix this!

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

In bac95f9d/ghc:

Yet another attempt at inferring the right quantification

TcSimplify.decideQuantification is truly a tricky function!
Trac #13509 showed that we were being over-eager with defaulting
of runtime-rep variables (levity polymorphism), which meant that
a program was wrongly rejected, and with a very odd error message
(c.f. Trac #13530)

I spent an unreasonably long time figuring out how to fix this
in a decent way, and ended up with a major refactoring of
decideQuantification, with a kock-on effect in simplifyInfer.

It is at least a bit more comprehensible now; but I still
can't say I like it.

comment:5 Changed 3 years ago by simonpj

Description: modified (diff)

comment:6 Changed 2 years ago by Richard Eisenberg <rae@…>

In 8e15e3d3/ghc:

Improve error messages around kind mismatches.

Previously, when canonicalizing (or unifying, in uType) a
heterogeneous equality, we emitted a kind equality and used the
resulting coercion to cast one side of the heterogeneous equality.

While sound, this led to terrible error messages. (See the bugs
listed below.) The problem is that using the coercion built from
the emitted kind equality is a bit like a wanted rewriting a wanted.
The solution is to keep heterogeneous equalities as irreducible.

See Note [Equalities with incompatible kinds] in TcCanonical.

This commit also removes a highly suspicious switch to FM_SubstOnly
when flattening in the kinds of a type variable. I have no idea
why this was there, other than as a holdover from pre-TypeInType.
I've not left a Note because there is simply no reason I can conceive
of that the FM_SubstOnly should be there.

One challenge with this patch is that the emitted derived equalities
might get emitted several times: when a heterogeneous equality is
in an implication and then gets floated out from the implication,
the Derived is present both in and out of the implication. This
causes a duplicate error message. (Test case:
typecheck/should_fail/T7368) Solution: track the provenance of
Derived constraints and refuse to float out a constraint that has
an insoluble Derived.

Lastly, this labels one test (dependent/should_fail/RAE_T32a)
as expect_broken, because the problem is really #12919. The
different handling of constraints in this patch exposes the error.

This fixes bugs #11198, #12373, #13530, and #13610.

test cases:

comment:7 Changed 2 years ago by goldfire

Resolution: fixed
Status: newclosed
Test Case: typecheck/should_fail/T13530
Note: See TracTickets for help on using tickets.