Opened 7 years ago
Closed 5 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 7 years ago by igloo
- difficulty set to Unknown
- Milestone set to 6.10 branch
comment:2 Changed 7 years ago by simonmar
- Architecture changed from Unknown to Unknown/Multiple
comment:3 Changed 7 years ago by simonmar
- Operating System changed from Unknown to Unknown/Multiple
comment:4 Changed 6 years ago by igloo
- Milestone changed from 6.10 branch to 6.12 branch
comment:5 Changed 5 years ago by igloo
- Milestone changed from 6.12 branch to 6.12.3
comment:6 Changed 5 years ago by igloo
- Milestone changed from 6.12.3 to 6.14.1
- Priority changed from normal to low
comment:7 Changed 5 years ago by claus
- Keywords vs removed
- Type of failure set to None/Unknown
- Version changed from 6.9 to 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 5 years ago by simonpj
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 5 years ago by igloo
- Owner set to simonpj
comment:10 Changed 5 years ago by simonpj
- Resolution set to fixed
- Status changed from new to closed
- Test Case set to 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.