Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,251
    • Issues 4,251
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 396
    • Merge Requests 396
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Wiki
    • New axioms
  • coincident overlap

Last edited by Tobias Dammers Mar 29, 2019
Page history New page

coincident overlap

Closed Type Families with Coincident Right-Hand Sides

In GHC 7.6, it is permitted to write something like this:

type instance F Int = Int
type instance F a   = a

These instances surely overlap, but in the case when they do, the right-hand sides coincide. This page explores the design space around this feature with an eye toward adding instance groups, as discussed here.

Coincident overlap within a closed type family

This section discusses a part of the "Concrete Proposal" on this page to patch a potential hole in Haskell's type system.

I (Richard) would like to be able to say this:

type family And (a :: Bool) (b :: Bool) :: Bool where
  And False a     = False
  And True  b     = b
  And c     False = False
  And d     True  = d
  And e     e     = e

According to the main page about closed type families, "We only match a type against an equation in a closed type family when no previous equation can unify against the type." Unfortunately, that kills us here. Consider reducing And f True. The first three branches clearly don't match. The fourth matches. But, the first two branches unify (i.e., they might apply later, depending on the instantiation for f), so we're stuck. Instead, we scan through the equations at the declaration and look to find compatible equations. Two equations are compatible if their right-hand sides match whenever their left-hand sides do. In the declaration above, all equations are compatible -- if a previous equation might apply later, we'd get the same result anyway, so we're OK. Then, during matching, we only check incompatible previous equations.

Another example is in order:

type family F a where
  F Int  = Int
  F Bool = Char
  F a    = a

The only incompatible pair of equations is F Bool and F a. Why? Let's consider this piece by piece. A use site that matches F Bool will never later match F Int, so F Int is compatible with F Bool. F Int might later match something that matches F a, but the right-hand sides coincide, so these equations are compatible. On the other hand, F Bool might also later match something that matches F a and the right-hand sides don't coincide, so these equations are not compatible. The upshot is that, if F a matches a use site, we have to make sure that F Bool cannot later apply. Otherwise, we can skip that check.

This is perhaps somewhat subtle, but it seems to be the right way to do it.

The ideas discussed here stem from posts by AntC, Andy Adams-Moran, and Richard on Richard's blog post on the subject.

Clone repository

GHC Home
GHC User's Guide

Joining In

Newcomers info
Mailing Lists & IRC
The GHC Team

Documentation

GHC Status Info
Working conventions
Building Guide
Debugging
Commentary

Wiki

Title Index
Recent Changes