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:
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
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