Skip to content
GitLab
Projects Groups Snippets
  • /
  • 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 5,242
    • Issues 5,242
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 565
    • Merge requests 565
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #7259
Closed
Open
Issue created Sep 21, 2012 by Simon Peyton Jones@simonpjDeveloper

Eta expansion of products in System FC

This ticket is to capture the ideas in these GHC-users threads: PolyKinds Aug 2012 and PolyKinds Sept 2012

  • We want to add eta-rules to FC. Sticking to pairs for now, that would amount to adding two new type functions (Fst, Snd), and three new, built-in axioms
	axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
	axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
	axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a

Generalising to arbitrary products looks feasible.

  • Adding these axioms would make FC inconsistent, because
	axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)

and that has two different type constructors on each side. However, I think is readily solved: see below under "Fixing Any"

  • Even in the absence of Any, it's not 100% obvious that adding the above eta axioms retains consistency of FC. I believe that Richard is volunteering to check this out. Right, Richard?

Type inference

I'm a little unclear about the implications for inference. One route might be this. Suppose we are trying to solve a constraint

     [W]  (a:'(k1,ks)) ~ '( t1, t2 )

where a is an untouchable type variable. (if it was touchable we'd simply unify it.) Then we can replace it with a constraint

    [W]   '(Fst a, Snd a) ~ '( t1, t2)

Is that it? Or do we need more? I'm a bit concerned about constraints like

    F a ~ e

where a:'(k1,k2), and we have a type instance like F '(a,b) = ...

Anything else?

I don't really want to eagerly eta-expand every type variable, because (a) we'll bloat the constraints and (b) we might get silly error messages. For (b) consider the insoluble constraint

    [W]  a~b

where a and b are both skolems of kind '(k1,k2). If we eta-expand both we'll get two insoluble constraints (Fst a ~ Fst b) and (Snd a ~ Snd b), and we DEFINITELY don't want to report that as a type error!

Someone pointed out that Agda grapples with this problem and we should talk to them.

Fixing Any

  • I think we can fix the Any problem readily by making Any into a type family, that has no instances. We certainly allow equalities with a type family application on the left and a type constructor on the right.

I have implemented this change already... it seems like a good plan.

  • Several people have asked why we need Any at all. Consider this source program
         reverse []

At what type should we instantiate reverse and the empty list []? Any type will do, but we must choose one; FC doesn't have unbound type variables. So I instantiate it at (Any *):

         reverse (Any *) ([] (Any *))

Why is Any poly-kinded? Because the above ambiguity situation sometimes arises at other kinds.

  • I'm betting that making Any into a family will mess up Richard's (entirely separate) use of (Any k) as a proxy for a kind argument k; because now (Any k1 ~ Any k2) does not entail (k1~k2). See also the module GHC.TypeLits in base.

We can't solve this by making Any to be an injective type family, because the use in TypeLits uses it in a type-class instance, and you can't match on type families!

Trac metadata
Trac field Value
Version 7.6.1
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking