Opened 4 years ago

Closed 4 years ago

#11248 closed bug (fixed)

Ambiguous Types with Constraint Synonyms

Reported by: crockeea Owned by:
Priority: high Milestone: 8.0.1
Component: Compiler Version: 7.10.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: polykinds/T11248
Blocked By: Blocking:
Related Tickets: #11330 Differential Rev(s):
Wiki Page:

Description (last modified by crockeea)

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.

Change History (10)

comment:1 Changed 4 years ago by crockeea

Description: modified (diff)

comment:2 Changed 4 years ago by simonpj

This too works in HEAD (and hence 8.0).

comment:3 Changed 4 years ago by Simon Peyton Jones <simonpj@…>

In 9d921d6/ghc:

Test Trac #11248, #11249

comment:4 Changed 4 years ago by simonpj

Test Case: polykinds/T11248

Regression test added. I doubt we'll fix the 7.10 branch unless there's a compelling reason.

comment:5 Changed 4 years ago by thomie

Milestone: 8.0.1
Resolution: fixed
Status: newclosed

comment:6 Changed 4 years ago by thomie

Resolution: fixed
Status: closednew

Actually,T11248 fails with core lint errors for WAY=optasm and WAY=hpc with HEAD (8.1.20151231):

 *** Core Lint errors : in result of Float out(FOS {Lam = Just 0,
                                                    Consts = True,
                                                    OverSatApps = True}) ***
 <no location info>: warning:
     [in body of lambda with binder eta_B1 :: CT
                                                r_a1JX (FLCM r_a1JX t_a1KA)]
     No alternatives for a case scrutinee in head-normal form: lvl_s1UO
                                                                 @ s_a1JY
                                                                 @ r_a1JX
                                                                 @ t_a1KA
                                                                 @~ (cobox_a1KB
                                                                     :: FMul
                                                                          (FGCD r_a1JX s_a1JY)
                                                                          (FDiv
                                                                             (FLCM r_a1JX t_a1KA)
                                                                             r_a1JX)
                                                                        ~# t_a1KA)
                                                                 @~ (cobox_a1KC
                                                                     :: FGCD r_a1JX t_a1KA
                                                                        ~# FGCD r_a1JX s_a1JY)
                                                                 @ s'_a1K1

comment:7 Changed 4 years ago by thomie

Priority: normalhigh

Core lint errors are bad, raising priority.

comment:8 Changed 4 years ago by Simon Peyton Jones <simonpj@…>

In 3c060f36/ghc:

Fix exprIsHNF (Trac #11248)

Blimey!  CoreUtils.exprIsHNFlike had not one but two bugs.

 * is_hnf_like treated coercion args like type args
   (result: exprIsHNF might wrongly say True)

 * app_is_value treated type args like value args
   (result: exprIsHNF might wrongly say False)

Bizarre.  This goes back to at least 2012. It's amazing that it
hasn't caused more trouble.

It was discovered by a Lint error when compiling Trac #11248 with -O.

comment:9 Changed 4 years ago by simonpj

Status: newmerge

Thanks for highlighting this. Fixed. Pls merge

Simon

comment:10 Changed 4 years ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.