[GHC] #11248: Ambiguous Types with Constraint Synonyms

[GHC]

#11248: Ambiguous Types with Constraint Synonyms
-------------------------------------+-------------------------------------
           Reporter:  crockeea       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.2
           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:
-------------------------------------+-------------------------------------
 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)

 type Ctx1 e r s e' r' =
   (Ctx2 e r s e' r', e' ~ (e ** (r' / r)))

 bug :: (Ctx1 e r s e' 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 move the `e' ~ ...` constraint from `Ctx1` to `Ctx2` or to
 the context of `bug`, it compiles as expected. Somehow, GHC misses the
 constraint when it is in `Ctx1`.

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