Opened 17 months ago

Closed 5 months ago

#12373 closed bug (fixed)

Type error but types match

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

Description

> unboxedsums git:(prim_sums_rebase_5) x cat primop_bug.hs
{-# LANGUAGE MagicHash, ScopedTypeVariables, UnboxedTuples #-}

module Main where

import GHC.MVar
import GHC.Prim
import GHC.Types

main :: IO ()
main = IO (\rw -> newMVar# rw) >> return ()

> unboxedsums git:(prim_sums_rebase_5) x ghc-stage1 primop_bug.hs -ddump-stg -ddump-cmm -ddump-to-file -fforce-recomp -dumpdir primop_fails -O -fprint-explicit-kinds
[1 of 1] Compiling Main             ( primop_bug.hs, primop_bug.o )

primop_bug.hs:10:19: error:
    • Couldn't match a lifted type with an unlifted type
      Expected type: (# State# RealWorld, MVar# RealWorld a0 #)
        Actual type: (# State# RealWorld, MVar# RealWorld a0 #)
    • In the expression: newMVar# rw
      In the first argument of ‘IO’, namely ‘(\ rw -> newMVar# rw)’
      In the first argument of ‘(>>)’, namely ‘IO (\ rw -> newMVar# rw)’

Tried with HEAD, 8.0.1.

Change History (5)

comment:1 Changed 17 months ago by simonpj

The error message is dire, but the error is real.

-- Type of data constructor for IO:
IO :: forall a. State# RealWorld -> (# State# RealWorld, a #)

-- Type of newMVar#
newMVar# :: forall b. State# s -> (# State# s, MVar# s b #)

So when we apply IO to newMVar# we have to instantiate the forall a with MVar# s b which isn't allowed.

comment:2 Changed 17 months ago by goldfire

This is probably #11198.

comment:3 Changed 17 months ago by simonpj

Yes, well spotted. It would be great to nail this since it keeps popping up.

comment:4 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:5 Changed 5 months ago by goldfire

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