[GHC] #11248: Ambiguous Types with Constraint Synonyms

[GHC]

#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