#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