Opened 5 years ago

Closed 5 years ago

#3043 closed bug (invalid)

An unrelated definition monomorphizes a type even without the MR

Reported by: Deewiant Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 6.10.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description

The following code:

{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies #-}

class Id a b | b -> a where id' :: a -> b
instance Id [Char] [Char] where id' = id

class Fst a where fst' :: a -> String
instance Fst ([Char],a) where fst' = fst

data Void a = Void

void :: (String,a) -> Void a
void _ = Void

fst'' (a,b) =
  let x = (id' a, b)
      y = void x :: Void Int -- remove this line and the code compiles
   in fst' x

Results in:

arst.hs:18:6:
    No instance for (Fst (b, Int))
      arising from a use of `fst'' at arst.hs:18:6-11
    Possible fix: add an instance declaration for (Fst (b, Int))
    In the expression: fst' x
    In the expression:
        let
          x = (id' a, b)
          y = void x :: Void Int
        in fst' x
    In the definition of `fst''':
        fst'' (a, b)
                = let
                    x = ...
                    y = ...
                  in fst' x

arst.hs:18:11:
    No instance for (Id [Char] b)
      arising from a use of `x' at arst.hs:18:11
    Possible fix: add an instance declaration for (Id [Char] b)
    In the first argument of `fst'', namely `x'
    In the expression: fst' x
    In the expression:
        let
          x = (id' a, b)
          y = void x :: Void Int
        in fst' x

It seems that the definition of y locks down the type of x somewhat even though the monomorphism restriction is disabled. If we remove the definition:

*Main> :t fst''
fst'' :: (Id t b, Fst (b, t1)) => (t, t1) -> String

To be completely honest I'm not sure whether the code should be accepted or not, since (Id t b, Fst (b, t1)) can't be satisfied. Only the fully monomorphic signature ([Char], Int) -> String, which is obtained with the definition of y in place and the monomorphism restriction enabled, works.

In any case, I think it's a bug that the results of the type check depend on whether y is defined or not: surely that shouldn't matter at all, no matter what the end result is.

Change History (1)

comment:1 Changed 5 years ago by simonpj

  • Difficulty set to Unknown
  • Resolution set to invalid
  • Status changed from new to closed

Your final remark isn't right in general. Consider:

f x = let y = x::Int
      in x && True

This is rejected, because x can't be both an Int and a Bool. But it'd be accepted if the binding for y was dropped. The type checker takes no notice of whether y is mentioned or not. (You might want it to, but I don't think it matters one way or the other in practice.)

In your example, since a and b are both mentioned in the right hand side of x, the type of x can't be generalised. Suppose a :: ta and b :: tb. Then the inferred type for x will be something like

  x :: forall c. Id ta c => (c, tb)

Now the type sig in y instantiates c to String, forces tb=Int, and generates a constraint (Id ta String). Now the fundep on Id forces ta=String.

That's as far as I have time to go today. I don't think this has anything to do with the MR.

Reopen if you disagree.

Simon

Note: See TracTickets for help on using tickets.