Another regression with type families

[rl]

Program (compile with ScopedTypeVariables):

type family H s a b

class D (G v) => C v where
  type G v
  type F v
  foo :: v -> H (F v) (G v) v

class D s where
  bar :: (forall t. Maybe t -> a) -> s -> H a s r -> r

call :: forall v. C v => F v -> v
call x = bar (\_ -> x)
             (undefined :: G v)
             (foo (undefined :: v))

bar' :: C v => (forall t. Maybe t -> F v) -> G v -> H (F v) (G v) v -> v
bar' = bar

The current head (even with today's typechecker patch) complains:

    Could not deduce (H a (G v) v ~ H (F v) (G v) v)
      from the context (C v)

But if I change bar to bar' in the rhs of foo, it all works fine. 6.12.3 accepts both programs.

[rl]

I meant the rhs of call, not rhs of foo.

[simonpj]

You didn't put all the flags. I used

{-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts #-}

module T4494 where

type family H s a b

class D (G v) => C v where
   type G v
   type F v
   foo :: v -> H (F v) (G v) v

class D s where
   bar :: (forall t. Maybe t -> a) -> s -> H a s r -> r

call :: forall v. C v => F v -> v
call x = bar (\_ -> x)
              (undefined :: G v)
              (foo (undefined :: v))

bar' :: C v => (forall t. Maybe t -> F v) -> G v -> H (F v) (G v) v -> v
bar' = bar

When I compile with HEAD I get

T4494.hs:16:10:
    Could not deduce (D (G v)) from the context (C v2)
      arising from a use of `bar'
    Possible fix:
      add (D (G v)) to the context of the type signature for `call'
      or add an instance declaration for (D (G v))
    In the expression:
      bar (\ _ -> x) (undefined :: G v) (foo (undefined :: v))
    In an equation for `call':
        call x = bar (\ _ -> x) (undefined :: G v) (foo (undefined :: v))

T4494.hs:18:16:
    Could not deduce (H (F v1) (G v1) v1 ~ H (F v2) (G v) v2)
      from the context (C v2)
    NB: `H' is a type function, and may not be injective
    In the third argument of `bar', namely `(foo (undefined :: v))'
    In the expression:
      bar (\ _ -> x) (undefined :: G v) (foo (undefined :: v))
    In an equation for `call':
        call x = bar (\ _ -> x) (undefined :: G v) (foo (undefined :: v))

With 6.12.3 I get

T4494.hs:16:9:
    No instance for (D (G v))
      arising from a use of `bar' at T4494.hs:(16,9)-(18,35)
    Possible fix: add an instance declaration for (D (G v))
    In the expression:
        bar (\ _ -> x) (undefined :: G v) (foo (undefined :: v))
    In the definition of `call':
        call x = bar (\ _ -> x) (undefined :: G v) (foo (undefined :: v))

T4494.hs:18:15:
    Couldn't match expected type `H (F v2) (G v) v2'
           against inferred type `H (F v1) (G v1) v1'
      NB: `H' is a type function, and may not be injective
    In the third argument of `bar', namely `(foo (undefined :: v))'
    In the expression:
        bar (\ _ -> x) (undefined :: G v) (foo (undefined :: v))
    In the definition of `call':
        call x = bar (\ _ -> x) (undefined :: G v) (foo (undefined :: v))

This look similar to me.

If I change bar to bar' in the rhs of call yields

T4494.hs:17:16:
    Could not deduce (G v ~ G v2) from the context (C v2)
    NB: `G' is a type function, and may not be injective
    In the second argument of `bar'', namely `(undefined :: G v)'
    In the expression:
      bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))
    In an equation for `call':
        call x = bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))

T4494.hs:18:16:
    Could not deduce (H (F v2) (G v2) v2 ~ H (F v1) (G v1) v1)
      from the context (C v2)
    NB: `H' is a type function, and may not be injective
    In the third argument of `bar'', namely `(foo (undefined :: v))'
    In the expression:
      bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))
    In an equation for `call':
        call x = bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))

I have not puzzled out whether these error messages are right, but so far I see no regression.

Simon

[rl]

Replying to simonpj:

You didn't put all the flags. I used

Indeed, sorry about that. But I did say that ScopedTypeVariables is required which you missed. The regression shows up then.

[simonpj]

I tried

{-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts, NoScopedTypeVariables #-}

module T4494 where

type family H s a b

class D (G v) => C v where
   type G v
   type F v
   foo :: v -> H (F v) (G v) v

class D s where
   bar :: (forall t. Maybe t -> a) -> s -> H a s r -> r

call :: forall v. C v => F v -> v
call x = bar' (\_ -> x)
              (undefined :: G v)
              (foo (undefined :: v))

bar' :: C v => (forall t. Maybe t -> F v) -> G v -> H (F v) (G v) v -> v
bar' = bar

and got this from HEAD

T4494.hs:17:16:
    Could not deduce (G v ~ G v2) from the context (C v2)
    NB: `G' is a type function, and may not be injective
    In the second argument of `bar'', namely `(undefined :: G v)'
    In the expression:
      bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))
    In an equation for `call':
        call x = bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))

T4494.hs:18:16:
    Could not deduce (H (F v2) (G v2) v2 ~ H (F v1) (G v1) v1)
      from the context (C v2)
    NB: `H' is a type function, and may not be injective
    In the third argument of `bar'', namely `(foo (undefined :: v))'
    In the expression:
      bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))
    In an equation for `call':
        call x = bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))

and this from 6.12.3:

T4494.hs:18:15:
    Couldn't match expected type `H (F v2) (G v2) v2'
           against inferred type `H (F v1) (G v1) v1'
      NB: `H' is a type function, and may not be injective
    In the third argument of `bar'', namely `(foo (undefined :: v))'
    In the expression:
        bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))
    In the definition of `call':
        call x = bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))

T4494.hs:18:15:
    Couldn't match expected type `G v2' against inferred type `G v'
      NB: `G' is a type function, and may not be injective
    In the third argument of `bar'', namely `(foo (undefined :: v))'
    In the expression:
        bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))
    In the definition of `call':
        call x = bar' (\ _ -> x) (undefined :: G v) (foo (undefined :: v))

Perhpas you can show exactly what you are doing, just as I am?

Simon

[rl]

This:

{-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts, ScopedTypeVariables #-}

module T4494 where

type family H s a b

class D (G v) => C v where
   type G v
   type F v
   foo :: v -> H (F v) (G v) v

class D s where
   bar :: (forall t. Maybe t -> a) -> s -> H a s r -> r

call :: forall v. C v => F v -> v
call x = bar' (\_ -> x)
              (undefined :: G v)
              (foo (undefined :: v))

bar' :: C v => (forall t. Maybe t -> F v) -> G v -> H (F v) (G v) v -> v
bar' = bar

Why did you use NoScopedTypeVariables instead of ScopedTypeVariables? Must be Friday evening!

[simonpj]

Oh. I used NoScopedTypeVariables because in the email it appears as !ScopedTypeVariables so I assumed you were using C negation. But acutally it was Trac markup!

Anyway, I tried the code you sent and it compiles just fine for me. Are you absolutely 100% certain that you are up to date with HEAD?

Simon

[rl]

I think this bug just doesn't want to be reported... Now you replaced bar by bar' in the rhs of call and I didn't replace it back. I'm sure we'll get there eventually.

Here is the code that doesn't compile with the head but does with 6.12.3. If you replace bar by bar' in the rhs of call it does compile with both. I've verified this twice so if anything goes wrong again it must be divine intervention.

{-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts, ScopedTypeVariables #-}

module T4494 where

type family H s a b

class D (G v) => C v where
   type G v
   type F v
   foo :: v -> H (F v) (G v) v

class D s where
   bar :: (forall t. Maybe t -> a) -> s -> H a s r -> r

call :: forall v. C v => F v -> v
call x = bar (\_ -> x)
              (undefined :: G v)
              (foo (undefined :: v))

bar' :: C v => (forall t. Maybe t -> F v) -> G v -> H (F v) (G v) v -> v
bar' = bar

[simonpj]

OK now I can reproduce it. Here's a cut down program.

{-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts,  ScopedTypeVariables #-}

module T4494 where

type family H s 
type family F v

bar :: (forall t. Maybe t -> a) -> H a -> Int
bar = error "urk"

call :: F Bool -> Int
call x = bar (\_ -> x) (undefined :: H (F Bool))

My compiler is build with DEBUG so it gives a more helpful error

T4494.hs:1:1:
    TERRIBLE ERROR: double set of meta type variable
    uf_ac3 := F Bool
    Old value = (uf_ac3, a)

Great catch, thanks.

Simon

[simonpj]

Fixed by

Mon Nov 15 12:15:40 GMT 2010  simonpj@microsoft.com
  * Ensure that unification variables alloc'd during solving are untouchable
  
  This fixes Trac #4494.  See Note [Extra TcsTv untouchables] in TcSimplify.

    M ./compiler/typecheck/TcCanonical.lhs -2 +2
    M ./compiler/typecheck/TcInteract.lhs -1 +9
    M ./compiler/typecheck/TcSMonad.lhs -8 +25
    M ./compiler/typecheck/TcSimplify.lhs -23 +73

Pls merge.

Simon

[igloo]

Merged.