Opened 6 years ago

Closed 4 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 Difficulty: Unknown
Test Case: indexed-types/should_fail/T2239 Blocked By:
Blocking: Related Tickets:

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 6 years ago by igloo

  • Difficulty set to Unknown
  • Milestone set to 6.10 branch

Thanks for the report.

comment:2 Changed 6 years ago by simonmar

  • Architecture changed from Unknown to Unknown/Multiple

comment:3 Changed 6 years ago by simonmar

  • Operating System changed from Unknown to Unknown/Multiple

comment:4 Changed 5 years ago by igloo

  • Milestone changed from 6.10 branch to 6.12 branch

comment:5 Changed 4 years ago by igloo

  • Milestone changed from 6.12 branch to 6.12.3

comment:6 Changed 4 years ago by igloo

  • Milestone changed from 6.12.3 to 6.14.1
  • Priority changed from normal to low

comment:7 Changed 4 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 4 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 4 years ago by igloo

  • Owner set to simonpj

comment:10 Changed 4 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

Note: See TracTickets for help on using tickets.