GitLab

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 (closed) 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.