[GHC] #11249: Type Synonyms cause Ambiguous Types

[GHC]

#11249: Type Synonyms cause Ambiguous Types
-------------------------------------+-------------------------------------
        Reporter:  crockeea          |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by crockeea:

Old description:

> The following code fails to compile:
>
> {{{
> {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies,
>              KindSignatures, ConstraintKinds #-}
>
> import GHC.TypeLits
>
> type a / b = FDiv a b
> type a ** b = FMul a b
>
> type family FDiv a b where
>   FDiv 11648 128 = 91
>
> type family FMul a b where
>   FMul 64 91 = 5824
>
> type family FGCD a b where
>   FGCD 128 448 = 64
>   FGCD 128 5824 = 64
>
> type family FLCM a b where
>   FLCM 128 5824 = 11648
>
> data CT (m :: Nat) (m' :: Nat)
> type H0 = 128
> type H1 = 448
> type H0' = 11648
> type H1' = 5824
>
> main' =
>   let x = undefined :: CT H0 H0'
>   in foo x :: CT H1 H1'
>
> foo x = bug x
>
> type Ctx2 e r s e' r' =
>   (e ~ FGCD r e', r' ~ FLCM r e', e ~ FGCD r s)
>
> bug :: (Ctx2 e r s e' r', e' ~ (e ** (FDiv r' r)))
>   => CT r r' -> CT s s'
> bug = undefined
> }}}
>
> with the error
>
> {{{
>     Could not deduce ((~) Nat (FGCD r e'0) (FGCD r s))
>     ...
>     The type variable ‘e'0’ is ambiguous
>     When checking that ‘foo’ has the inferred type
>       foo :: forall (r :: Nat) (s :: Nat) (s' :: Nat) (e' :: Nat).
>              ((~) Nat (FGCD r s) (FGCD r e'),
>               (~) Nat (FMul (FGCD r s) (FDiv (FLCM r e') r)) e') =>
>              CT r (FLCM r e') -> CT s s'
>     Probable cause: the inferred type is ambiguous
> }}}
>
> However, if I change the definition of `bug` to:
>
> {{{
> bug :: (Ctx2 e r s e' r', e' ~ (e ** (r' / r)))
>   => CT r r' -> CT s s'
> bug = undefined
> }}}
>
> that is, I use the type synonym `/` for `FDiv`, then the code suddenly
> compiles. This seems like a different bug than #11248 because that ticket
> is about transitivity of constraint synonyms, while this example is
> broken simply by using a type synonym.

New description:

 The following code fails to compile:

 {{{
 {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies,
              KindSignatures, ConstraintKinds #-}

 import GHC.TypeLits

 type a / b = FDiv a b
 type a ** b = FMul a b

 type family FDiv a b where
   FDiv 11648 128 = 91

 type family FMul a b where
   FMul 64 91 = 5824

 type family FGCD a b where
   FGCD 128 448 = 64
   FGCD 128 5824 = 64

 type family FLCM a b where
   FLCM 128 5824 = 11648

 data CT (m :: Nat) (m' :: Nat)
 type H0 = 128
 type H1 = 448
 type H0' = 11648
 type H1' = 5824

 main' =
   let x = undefined :: CT H0 H0'
   in foo x :: CT H1 H1'

 foo x = bug x

 type Ctx2 e r s e' r' =
   (e ~ FGCD r e', r' ~ FLCM r e', e ~ FGCD r s)

 bug :: (Ctx2 e r s e' r', e' ~ (e ** (FDiv r' r)))
   => CT r r' -> CT s s'
 bug = undefined
 }}}

 with the error

 {{{
     Could not deduce ((~) Nat (FGCD r e'0) (FGCD r s))
     ...
     The type variable ‘e'0’ is ambiguous
     When checking that ‘foo’ has the inferred type
       foo :: forall (r :: Nat) (s :: Nat) (s' :: Nat) (e' :: Nat).
              ((~) Nat (FGCD r s) (FGCD r e'),
               (~) Nat (FMul (FGCD r s) (FDiv (FLCM r e') r)) e') =>
              CT r (FLCM r e') -> CT s s'
     Probable cause: the inferred type is ambiguous
 }}}

 However, if I change the definition of `bug` to:

 {{{
 bug :: (Ctx2 e r s e' r', e' ~ (e ** (r' / r)))
   => CT r r' -> CT s s'
 bug = undefined
 }}}

 that is, I use the type synonym `/` for `FDiv`, then the code suddenly
 compiles. This seems like a different bug than #11248 because that ticket
 is about transitivity of constraint synonyms, while this example is broken
 simply by using a type synonym.

 It's possible that this is also related to #10338, but I'm not sure.

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11249#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler