Failed deriving for GADT

[GoogleCodeExporter]

[Reported by Hongbo Zhang]

  I rolled back my compiler to 7.2.1
tried to derive such data type

data MyExp a where
  A :: Int -> MyExp Int
  B :: Char -> MyExp Char
  F :: MyExp Int -> MyExp Char -> MyExp (Int,Char)
  C :: MyExp a -> MyExp b -> MyExp (a,b)
  D :: a -> MyExp a
data MyFoo a where
  Bar  :: Int -> MyFoo Int
  Bar2 :: MyFoo b -> MyFoo [b]
  Bar3 :: MyFoo c -> MyFoo d -> MyFoo (c,d)
data Test b where
  Foo1 :: Test a -> Test (a,b)
  Foo2 :: Char -> Test Char
Only the last succeed,
I have attached the source file, and error information.
Can you help me to make it compile? Many thanks
The first gives out error messages like this
/Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1:
    Could not deduce (b1 ~ Char)
    from the context (Rep a)
      bound by the type signature for rMyExp :: Rep a => R (MyExp a)
      at /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1-18
    or from (Rep b, Rep b1)
      bound by a pattern with constructor
                Result2 :: forall (c_a2HT :: * -> * -> *) a_a2HU b_a2HV
b_a2HW.
                            (Rep b_a2HV, Rep b_a2HW) =>
                            (a_a2HU :=: c_a2HT b_a2HV b_a2HW) -> Res2
c_a2HT a_a2HU,
              in a case alternative
      at /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1-18
      `b1' is a rigid type variable bound by
          a pattern with constructor
            Result2 :: forall (c_a2HT :: * -> * -> *) a_a2HU b_a2HV b_a2HW.
                        (Rep b_a2HV, Rep b_a2HW) =>
                        (a_a2HU :=: c_a2HT b_a2HV b_a2HW) -> Res2 c_a2HT
a_a2HU,
          in a case alternative
          at
/Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1
    Expected type: a :=: (Int, Char)
      Actual type: a :=: (b, b1)
    In the pattern: Refl :: :=: a_a2H4 (Int, Char)
    In the pattern: Result2 (Refl :: :=: a_a2H4 (Int, Char))

/Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1:
    Could not deduce (b ~ Int)
    from the context (Rep a)
      bound by the type signature for rMyExp :: Rep a => R (MyExp a)
      at /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1-18
    or from (Rep b, Rep b1)
      bound by a pattern with constructor
                Result2 :: forall (c_a2HT :: * -> * -> *) a_a2HU b_a2HV
b_a2HW.
                            (Rep b_a2HV, Rep b_a2HW) =>
                            (a_a2HU :=: c_a2HT b_a2HV b_a2HW) -> Res2
c_a2HT a_a2HU,
              in a case alternative
      at /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1-18
      `b' is a rigid type variable bound by
          a pattern with constructor
            Result2 :: forall (c_a2HT :: * -> * -> *) a_a2HU b_a2HV b_a2HW.
                      (Rep b_a2HV, Rep b_a2HW) =>
                      (a_a2HU :=: c_a2HT b_a2HV b_a2HW) -> Res2 c_a2HT
a_a2HU,
          in a case alternative
          at /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1
    Expected type: a :=: (Int, Char)
      Actual type: a :=: (b, b1)
    In the pattern: Refl :: :=: a_a2H4 (Int, Char)
    In the pattern: Result2 (Refl :: :=: a_a2H4 (Int, Char))

/Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1:
    Could not deduce (b1 ~ Char)
    from the context (Rep a)
      bound by the type signature for
                rMyExp1 :: Rep a =>
                            ctx Int
                            -> ctx Char
                            -> (ctx (MyExp Int), ctx (MyExp Char))
                            -> R1 ctx (MyExp a)
      at /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1-18
    or from (Rep b, Rep b1)
      bound by a pattern with constructor
                Result2 :: forall (c_a2HT :: * -> * -> *) a_a2HU b_a2HV
b_a2HW.
                            (Rep b_a2HV, Rep b_a2HW) =>
                            (a_a2HU :=: c_a2HT b_a2HV b_a2HW) -> Res2
c_a2HT a_a2HU,
              in a case alternative
      at /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1-18
      `b1' is a rigid type variable bound by
          a pattern with constructor
            Result2 :: forall (c_a2HT :: * -> * -> *) a_a2HU b_a2HV b_a2HW.
                        (Rep b_a2HV, Rep b_a2HW) =>
                        (a_a2HU :=: c_a2HT b_a2HV b_a2HW) -> Res2 c_a2HT
a_a2HU,
          in a case alternative
          at
/Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1
    Expected type: a :=: (Int, Char)
      Actual type: a :=: (b, b1)
    In the pattern: Refl :: :=: a_a2H4 (Int, Char)
    In the pattern: Result2 (Refl :: :=: a_a2H4 (Int, Char))

/Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1:
    Could not deduce (b ~ Int)
    from the context (Rep a)
      bound by the type signature for
                rMyExp1 :: Rep a =>
                            ctx Int
                            -> ctx Char
                            -> (ctx (MyExp Int), ctx (MyExp Char))
                            -> R1 ctx (MyExp a)
      at /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1-18
    or from (Rep b, Rep b1)
      bound by a pattern with constructor
                Result2 :: forall (c_a2HT :: * -> * -> *) a_a2HU b_a2HV
b_a2HW.
                            (Rep b_a2HV, Rep b_a2HW) =>
                            (a_a2HU :=: c_a2HT b_a2HV b_a2HW) -> Res2
c_a2HT a_a2HU,
              in a case alternative
      at /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1-18
      `b' is a rigid type variable bound by
          a pattern with constructor
            Result2 :: forall (c_a2HT :: * -> * -> *) a_a2HU b_a2HV b_a2HW.
                      (Rep b_a2HV, Rep b_a2HW) =>
                      (a_a2HU :=: c_a2HT b_a2HV b_a2HW) -> Res2 c_a2HT
a_a2HU,
          in a case alternative
          at /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1
    Expected type: a :=: (Int, Char)
      Actual type: a :=: (b, b1)
    In the pattern: Refl :: :=: a_a2H4 (Int, Char)
    In the pattern: Result2 (Refl :: :=: a_a2H4 (Int, Char))
Failed, modules loaded: none.

The second gives out error messages like this:
Multiple declarations of `Generics.RepLib.RepExperiment.dict'
    Declared at:
/Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1

 /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1

/Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1:
    Multiple declarations of `Generics.RepLib.RepExperiment.Sat'
    Declared at:
/Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1

 /Users/bob/SourceCode/course/is/expriment/RepExperiment.hs:41:1
Failed, modules loaded: none.

Original issue reported on code.google.com by [email protected] on 19 Sep 2012 at 4:06