[GHC] #11249: Type Synonyms cause Ambiguous Types

17 Dec 2015

      #11249: Type Synonyms cause Ambiguous Types
-------------------------------------+-------------------------------------
           Reporter:  crockeea       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.2
           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:
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11249
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler