#11248: Ambiguous Types with Constraint Synonyms -------------------------------------+------------------------------------- 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)

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`.

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) 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. -- -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11248#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#11248: Ambiguous Types with Constraint Synonyms -------------------------------------+------------------------------------- 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 <simonpj@…>): In [changeset:"9d921d6bfeec8320f7ad5e4532bf4edadc7f92cd/ghc" 9d921d6/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="9d921d6bfeec8320f7ad5e4532bf4edadc7f92cd" Test Trac #11248, #11249 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11248#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#11248: Ambiguous Types with Constraint Synonyms -------------------------------------+------------------------------------- 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/T11248 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/11248#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#11248: Ambiguous Types with Constraint Synonyms -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | polykinds/T11248 Blocked By: | Blocking: Related Tickets: #11330 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * priority: normal => high Comment: Core lint errors are bad, raising priority. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11248#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler

#11248: Ambiguous Types with Constraint Synonyms -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: merge Priority: high | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | polykinds/T11248 Blocked By: | Blocking: Related Tickets: #11330 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge Comment: Thanks for highlighting this. Fixed. Pls merge Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11248#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler