Opened 6 years ago

Closed 6 years ago

Last modified 6 years ago

#2044 closed merge (fixed)

"Can't unify" error in debugger

Reported by: r6144 Owned by: igloo
Priority: normal Milestone: 6.8.3
Component: GHCi Version: 6.8.2
Keywords: Cc: mnislaih@…
Operating System: Linux Architecture: x86
Type of failure: Difficulty: Unknown
Test Case: print033 Blocked By:
Blocking: Related Tickets:

Description

Debugging the attached array1.hs under GHCi gives the following error:

[haskell]$ ghci
GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
Prelude> :load array1.hs 
[1 of 1] Compiling Main             ( array1.hs, interpreted )
Ok, modules loaded: Main.
*Main> :break rsRandomArray 
Breakpoint 0 activated at array1.hs:(31,0)-(42,79)
*Main> main
Loading package array-0.1.0.0 ... linking ... done.
Loading package old-locale-1.0.0.0 ... linking ... done.
Loading package old-time-1.0.0.0 ... linking ... done.
Loading package random-1.0.0.0 ... linking ... done.
Array 1: array Stopped at array1.hs:(31,0)-(42,79)
_result :: ST s (UArray Idx Double) = _
[array1.hs:(31,0)-(42,79)] *Main> :step
Stopped at array1.hs:31:21-53
ghc-6.8.2: panic! (the 'impossible' happened)
  (GHC version 6.8.2 for i386-unknown-linux):
        Can't unify

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

[array1.hs:31:21-53] *Main> :quit
Leaving GHCi.

I'm running Fedora 8 with gcc version 4.1.2 20070925 (Red Hat 4.1.2-33) and ghc-6.8.2-2.fc8.

Attachments (2)

array1.hs (2.5 KB) - added by r6144 6 years ago.
The offending program
array1-orig.hs (2.7 KB) - added by r6144 6 years ago.
Modified version of array1.hs that compiles with ghc 6.9.20080323

Download all attachments as: .zip

Change History (18)

Changed 6 years ago by r6144

The offending program

comment:1 Changed 6 years ago by igloo

  • Difficulty set to Unknown
  • Milestone set to 6.8.3

Thanks for the report; I can reproduce the problem.

comment:2 Changed 6 years ago by igloo

  • Owner set to simonpj

...but not with the HEAD.

This program:

{-# LANGUAGE ScopedTypeVariables, ExistentialQuantification #-}

import Control.Monad.ST.Strict
import Data.Array.ST

rsRandom :: ST s a
rsRandom = undefined

write :: Int -> ST s (forall ss . (STUArray ss Int Double) -> ST ss ())
write i = rsRandom >>= \x -> return (\buf -> writeArray buf i x)

is accepted by the 6.8 branch, but not the HEAD. I'd expect it to be rejected too (x is monomorphic, and generalisation won't make a higher rank type), so I think the HEAD is right, but I will let Simon PJ have the last word...

I don't think this is worth fixing just for 6.8.3, unless there are other programs that the HEAD also accepts that trigger the problem, so if the program ought to be rejected then I think that we can close this ticket.

comment:3 Changed 6 years ago by r6144

-XImpredicativeTypes (implied by -fglasgow-exts) appears to be necessary for array1.hs as well as igloo's simpler example.

To make the original array1.hs compile with GHC 6.9.20080323, I have to expand the do statements involving polymorphic lambda-bound variables, e.g. "do { w <- writeRandoms ; return (newArray_ (0,n-1) >>= w) }" into "writeRandoms >>= \w -> return (newArray_ (0,n-1) >>= w)". If I understand correctly, -XImpredicativeTypes allows w to be polymorphic.

After this modification, array1.hs (called array1-orig.hs below) compiles, but the original problem persists:

[haskell]$ ~/apps/ghc-6.9.20080323/bin/ghci
GHCi, version 6.9.20080323: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
Prelude> :load array1-orig.hs
[1 of 1] Compiling Main             ( array1-orig.hs, interpreted )
Ok, modules loaded: Main.
*Main> :break rsRandomArray
Breakpoint 0 activated at array1-orig.hs:(32,0)-(43,86)
*Main> main
Loading package array-0.1 ... linking ... done.
Loading package old-locale-1.0 ... linking ... done.
Loading package old-time-1.0 ... linking ... done.
Loading package random-1.0 ... linking ... done.
Array 1: array Stopped at array1-orig.hs:(32,0)-(43,86)
_result :: ST s (UArray Idx Double) = _
[array1-orig.hs:(32,0)-(43,86)] *Main> :step
Stopped at array1-orig.hs:32:21-53
ghc-6.9.20080323: panic! (the 'impossible' happened)
  (GHC version 6.9.20080323 for i386-unknown-linux):
        Can't unify

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

[array1-orig.hs:32:21-53] *Main> :quit
Leaving GHCi.
[

Changed 6 years ago by r6144

Modified version of array1.hs that compiles with ghc 6.9.20080323

comment:4 Changed 6 years ago by simonpj

  • Owner changed from simonpj to pepe

The "can't unify" message comes from RtsClosureInspect, which is Pepe and Simon's debugger. I suspect it's confused by the for-all in the type.

Ian is right, incidentally, that the short program he gives should be rejected unless you specify -XImpredicativeTypes.

So I'm assigning this bug to Pepe.

Simon

comment:5 Changed 6 years ago by simonpj

  • Cc mnislaih@… added

And adding Pepe to the cc list. Simon

comment:6 Changed 6 years ago by mnislaih

  • Owner changed from pepe to mnislaih
  • Status changed from new to assigned

Thanks for CC'ing, I had missed this ticket.

At first I though this problem was an instance of #1995, but it turns out your suspicion was right.
The RTTI mechanism panics when trying to reconstruct the type for buildBuf in line 3.
This is the 'full' error obtained via initTcPrintErrors :

Top level:
    Cannot match a monotype with `ST s (forall s'. ST s' (STUArray s' Idx Double))'
      Expected type: ST s (forall s'. ST s' (STUArray s' Idx Double))
      Inferred type: t
ghc-6.9.20080404: panic! (the 'impossible' happened)
  (GHC version 6.9.20080404 for i386-apple-darwin):
        Can't unify

So GHC is refusing to unify the tyvar with an impredicative type. This tyvar is created as follows:

newVar kind = mkTyVarTy `fmap` newFlexiTyVar kind 

in this case with kind argType.

How should the tyvars used by the RTTI mechanism be created to handle this situation ?

And, do we need to handle it at all?
At runtime we handle values, which are monomorphically typed. It looks to me that the type recovered for buildBuf should be just:

buildBuf :: ST s (ST s' (STUArray s' Idx Double)

Does that make sense?

comment:7 Changed 6 years ago by simonpj

I don't fully grok the debugger type reconstruction, but newBoxyTyVar might be what you want. It does not insist on unifying with a monotype.

Simon

comment:8 Changed 6 years ago by mnislaih

The way I see it, :print is dealing with concrete values here, and a value has a factual type. It does not make sense to impose restrictions like class predicates or higher rank foralls on the value's type. Thus I believe those higher-rank foralls should be dropped.

If we have a function type on the other hand, the foralls should be respected. But :print should not touch the types of function types anyway.

comment:9 Changed 6 years ago by simonpj

A value can be

  • A basic type like Int
  • A function, like Int -> Int
  • An overloaded function like forall a. Eq a => a -> a, or non-function like forall a. Num a => a
  • A polymorphic function like forall a. [a] -> [a], or non-function like forall a. [a]
  • With impredicative polymorphism, a data structure containing polymorphic values, like [forall a. a ->a] or [forall a. Eq a = a -> a]

These are all perfectly concrete values. A function of type forall a. Eq a => a -> a takes two arguments not one, for example. I'm not sure what you mean by a "factual type", nor what you mean by "should not touch the types of function types".

It's true that in the representation, the foralls are dropped, so a function of type forall a. [a] -> [a] takes just one argument.

Simon

comment:10 Changed 6 years ago by mnislaih

Sorry, by "should not touch the types of function types", I mean that :print can only reconstruct types for non-function values, and thus it does not deal with the types of function values. A function value for :print is a Fun closure.

When a call to a polymorphic function is done, the outer level foralls are instantiated and eliminated. The role of :print is to find out what is the particular instantiation. But this is true for outer level foralls only. For higher rank foralls inside Type Constructors, that is, impredicative types (is this the correct terminology ?) I am in doubt, since I don't understand the implications of impredicative types. These foralls are restrictions too after all, which have already been checked. Is it ok to drop them? I need to do some reading.

By the way an interesting question about typeclass predicates.
Suppose we have a function type forall a. Show a => a -> a. If :print recovers a concrete type for the first arg., then by assumption this type is an instance of Show. If :print does not recover a type, it would be nice to pack the dictionary, which :print has access to, and say "x has type Show a => a and you can call show for it in GHCi", but I don't see how that can be expressed. But even more, maybe can we use the dictionaries themselves for recovering more types ?

comment:11 Changed 6 years ago by simonpj

I don't understand your debugger well enough to give you a coherent response. My guess is that newBoxyTyVar will get you past the current "cant unify", albeit perhaps present some other part of your debugger with a polymorphic type it didn't expect.

I suggest you have a chat with Simon M and/or Bernie initially.

Meanwhile this bug is only going to affect people using the more exotic GHC extensions, I think.

Still, doing something less unfriendly than crashing would be a useful step forward, and you can probably do that regardless?

Simon

comment:12 Changed 6 years ago by mnislaih

I tried with boxy tyvars and that makes the trick almost.
The problem now is in the side-effect free unification procedure living in types/Unify.hs (previously TcGadt?.hs). It fails when asked, at some point later in the debugger, to unify the type of rsRandomArray with itself.

I think I will simply switch to boxyUnify here too, and that should suffice to close this ticket.

comment:13 Changed 6 years ago by mnislaih

Oops, I mean the type of buildBuf

buildBuf :: ST s (forall s'. ST s' (STUArray s' Idx Double))

comment:14 Changed 6 years ago by mnislaih

  • Cc igloo@… added
  • Owner changed from mnislaih to igloo
  • Status changed from assigned to new
  • Type changed from bug to merge

Fixed, merge to stable

Mon Apr 21 10:13:22 PDT 2008  pepe <mnislaih@gmail.com>
 * Fix #2044 (:printing impredicatively typed things)

comment:15 Changed 6 years ago by igloo

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to print033

Merged

comment:16 Changed 6 years ago by igloo

  • Cc igloo@… removed
Note: See TracTickets for help on using tickets.