Opened 8 months ago

Closed 5 months ago

#13610 closed bug (fixed)

Unhelpful error messages about lifted and unlifted types

Reported by: nomeata Owned by:
Priority: low Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.1
Keywords: Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T13610
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I wrote this code:

{-# LANGUAGE MagicHash #-}
import GHC.Prim
import GHC.Types

main = do
    let primDouble = 0.42## :: Double#
    let double = 0.42 :: Double
    IO (\s -> mkWeakNoFinalizer# double () s)

and I get this error message:

WeakDouble.hs:8:15: error:
    • Couldn't match a lifted type with an unlifted type
      Expected type: (# State# RealWorld, Weak# () #)
        Actual type: (# State# RealWorld, Weak# () #)
    • In the expression: mkWeakNoFinalizer# double () s
      In the first argument of ‘IO’, namely
        ‘(\ s -> mkWeakNoFinalizer# double () s)’
      In a stmt of a 'do' block:
        IO (\ s -> mkWeakNoFinalizer# double () s)

with -fprint-explicit-kinds. (Without the flag, it looks the same, but tells me to use this flag…).

Change History (8)

comment:1 Changed 8 months ago by nomeata

Ah, the problem is that IO’s type expects the second component of the tuple to be lifted, but Weak# is not. So the code is indeed bogus, but the error message is not very helpful.

comment:2 Changed 8 months ago by goldfire

I guess the question is this: should -fprint-explicit-kinds print unboxed tuple types in prefix so that the levity arguments are displayed? I think: no. But perhaps -fprint-explicit-runtime-reps should, and GHC should be taught to tell the user about this flag instead of -fprint-explicit-kinds in this scenario.

comment:3 Changed 8 months ago by nomeata

Priority: normallow

I am not sure if printing type prefixes would have improved manners. What would it say? Maybe

      Expected type: (#,#) VoidRep LiftedRep (State# RealWorld) (Weak# ())
        Actual type: (#,#) VoidRep PrimRep   (State# RealWorld) (Weak# ())

But the “actual type” is not well-kinded; it cannot really be the “actual type” of anything. So it seems that something went wrong earlier during type inference?

I guess something along these lines would have been more helpful:

WeakDouble.hs:8:15: error:
    • Couldn't match a lifted type with an unlifted type
      Expected type representation: LiftedRep
        Actual type representation: PrimRep
    • In the second element of the unlifted tuple
    • In the type of the expression: mkWeakNoFinalizer# double () s

Anyways; this was not triggered by writing real code, so I’ll lower the priority.

comment:4 Changed 8 months ago by goldfire

This may be fixed by the fix to #11198.

comment:5 Changed 8 months ago by bgamari

Milestone: 8.2.1

comment:6 Changed 6 months ago by bgamari

Milestone: 8.2.18.4.1

Bumping off to 8.4.

comment:7 Changed 5 months 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:
typecheck/should_fail/{T8262,T8603,tcail122,T12373,T13530,T13610}

comment:8 Changed 5 months ago by goldfire

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