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,334
    • Issues 4,334
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 368
    • Merge Requests 368
  • 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
  • Issues
  • #9117

Closed
Open
Opened May 15, 2014 by Richard Eisenberg@raeDeveloper

Coercible constraint solver misses one

When I say

import Data.Type.Coercion
import Data.Coerce

eta :: Coercible f g => Coercion (f a) (g a)
eta = Coercion

I get

    Could not coerce from ‘f a’ to ‘g a’
      because ‘f a’ and ‘g a’ are different types.
      arising from a use of ‘Coercion’
    from the context (Coercible f g)
      bound by the type signature for
                 eta :: Coercible f g => Coercion (f a) (g a)
      at /Users/rae/temp/Roles.hs:6:8-44
    In the expression: Coercion
    In an equation for ‘eta’: eta = Coercion

But, this coercion is easily expressible in Core. If (co :: f ~R# g) then (co <a> :: f a ~R# g a), where <a> is the notation for a reflexivity coercion for the type a. The constraint solver should be able to do this.

Trac metadata
Trac field Value
Version 7.8.2
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#9117