#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

#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: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"9d921d6bfeec8320f7ad5e4532bf4edadc7f92cd/ghc" 9d921d6/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="9d921d6bfeec8320f7ad5e4532bf4edadc7f92cd" Test Trac #11248, #11249 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11249#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11249: Type Synonyms cause Ambiguous Types -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: closed Priority: normal | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | polykinds/T11249 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * status: new => closed * resolution: => fixed * milestone: => 8.0.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11249#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler