Skip to content

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.

Edited by Eric Crockett
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information