Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,824
    • Issues 4,824
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 448
    • Merge requests 448
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
    • Value stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #11248

Closed
Open
Created Dec 18, 2015 by Eric Crockett@crockeeaReporter

Ambiguous Types with Constraint Synonyms

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.

Edited Mar 10, 2019 by Eric Crockett
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking