## Ambiguous Types with Constraint Synonyms

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`

.

I don't think this is #10338, but someone who knows more about the innards of GHC can verify.