Opened 9 years ago
Closed 6 years ago
#2239 closed bug (fixed)
lack of improvement/reduction with TFs
Reported by: | claus | Owned by: | simonpj |
---|---|---|---|
Priority: | low | Milestone: | 7.0.1 |
Component: | Compiler (Type checker) | Version: | 6.12.3 |
Keywords: | TF FD | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | indexed-types/should_fail/T2239 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeFamilies #-} data A = A data B = B class C a where c :: a -> String instance C Bool where c _ = "Bool" instance C Char where c _ = "Char" -- via TFs type family TF a type instance TF A = Char type instance TF B = Bool tf :: forall a b. (b ~ TF a,C b) => a -> String tf a = c (undefined:: b) -- via FDs class FD a b | a -> b instance FD A Char instance FD B Bool fd :: forall a b. (FD a b,C b) => a -> String fd a = c (undefined:: b)
for some reason, the TF version doesn't work as well as the FD version:
*Main> fd A "Char" *Main> fd B "Bool" *Main> tf A <interactive>:1:0: No instance for (C (TF A)) arising from a use of `tf' at <interactive>:1:0-3 Possible fix: add an instance declaration for (C (TF A)) In the expression: tf A In the definition of `it': it = tf A *Main> :t undefined :: (b~TF A)=>b undefined :: (b~TF A)=>b :: TF A *Main> :t undefined :: (FD A b)=>b undefined :: (FD A b)=>b :: Char
this is with GHCi, version 6.9.20080217
.
the result of the TF is "known", even if not used:
*Main> :t undefined :: (b~TF A,b~Char)=>b undefined :: (b~TF A,b~Char)=>b :: TF A *Main> :t undefined :: (b~TF A,b~Bool)=>b <interactive>:1:0: Couldn't match expected type `Bool' against inferred type `Char'
Change History (10)
comment:1 Changed 9 years ago by
difficulty: | → Unknown |
---|---|
Milestone: | → 6.10 branch |
comment:2 Changed 8 years ago by
Architecture: | Unknown → Unknown/Multiple |
---|
comment:3 Changed 8 years ago by
Operating System: | Unknown → Unknown/Multiple |
---|
comment:4 Changed 8 years ago by
Milestone: | 6.10 branch → 6.12 branch |
---|
comment:5 Changed 7 years ago by
Milestone: | 6.12 branch → 6.12.3 |
---|
comment:6 Changed 7 years ago by
Milestone: | 6.12.3 → 6.14.1 |
---|---|
Priority: | normal → low |
comment:7 Changed 7 years ago by
Keywords: | vs removed |
---|---|
Type of failure: | → None/Unknown |
Version: | 6.9 → 6.12.3 |
Though there was no recorded activity on this ticket, there seem to have been some changes (using 6.12.3). Perhaps this ticket should be brought to the attention of whoever is working in that area?-)
Good news: the tf A
and tf B
examples now seem to work.
Not so good news: there are still examples where improvement differs between TFs and FDs (see below); also, without comment it is not clear whether the progress is accidental.
Here is another example that still shows a difference with 6.12.3. We define an FD-based type equality and a couple of examples
{-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} class MyEq a b | a->b, b->a instance MyEq a a simpleFD = id :: (forall b. MyEq b Bool => b->b) simpleTF = id :: (forall b. b~Bool => b->b) complexFD = id :: (forall b. MyEq b Bool => b->b) -> (forall b. MyEq b Bool => b->b) {- doesn't typecheck: complexTF = id :: (forall b. b~Bool => b->b) -> (forall b. b~Bool => b->b) -}
and then both the TF and the FD type equality work for the simple case, but only the FD one works for the complex one
*Main> :t simpleFD simpleFD :: Bool -> Bool *Main> :t simpleTF simpleTF :: Bool -> Bool *Main> :t complexFD complexFD :: (forall b. (MyEq b Bool) => b -> b) -> Bool -> Bool
(though even with complexFD
, the inner forall b
does not get instantiated). Reloading the module with complexTF included leads to
C:\Users\claus\Desktop\tmp\show-eq.hs:17:12: Couldn't match expected type `forall b. (b ~ Bool) => b -> b' against inferred type `forall b. (b ~ Bool) => b -> b' Expected type: forall b. (b ~ Bool) => b -> b Inferred type: forall b. (b ~ Bool) => b -> b In the expression: id :: (forall b. (b ~ Bool) => b -> b) -> (forall b. (b ~ Bool) => b -> b) In the definition of `complexTF': complexTF = id :: (forall b. (b ~ Bool) => b -> b) -> (forall b. (b ~ Bool) => b -> b)
comment:8 Changed 7 years ago by
Thanks Claus. This ticket is firmly on my list of tickets to look at once we have the new inference machinery working. It's most implemented now; next is to start testing.
Simon
comment:9 Changed 7 years ago by
Owner: | set to simonpj |
---|
comment:10 Changed 6 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → indexed-types/should_fail/T2239 |
The new typechecker is happy with all these except complexFD
and complexTF
which fail in the same way
T2239.hs:43:13: Couldn't match expected type `b -> b' with actual type `forall b1. MyEq b1 Bool => b1 -> b1' Expected type: (forall b1. MyEq b1 Bool => b1 -> b1) -> b -> b Actual type: (forall b1. MyEq b1 Bool => b1 -> b1) -> forall b1. MyEq b1 Bool => b1 -> b1 In the expression: id :: (forall b. MyEq b Bool => b -> b) -> (forall b. MyEq b Bool => b -> b) In an equation for `complexFD': complexFD = id :: (forall b. MyEq b Bool => b -> b) -> (forall b. MyEq b Bool => b -> b) T2239.hs:47:13: Couldn't match expected type `b -> b' with actual type `forall b1. b1 ~ Bool => b1 -> b1' Expected type: (forall b1. b1 ~ Bool => b1 -> b1) -> b -> b Actual type: (forall b1. b1 ~ Bool => b1 -> b1) -> forall b1. b1 ~ Bool => b1 -> b1 In the expression: id :: (forall b. b ~ Bool => b -> b) -> (forall b. b ~ Bool => b -> b) In an equation for `complexTF': complexTF = id :: (forall b. b ~ Bool => b -> b) -> (forall b. b ~ Bool => b -> b)
To make them work you need to instantiate id
at a polytype, which involves impredicativity.
I've added the examples as a regression test though.
Simon
Thanks for the report.