Opened 3 years ago

Closed 3 years ago

#10285 closed bug (fixed)

Bug in Coerciible

Reported by: simonpj Owned by: goldfire
Priority: highest Milestone: 7.10.2
Component: Compiler Version: 7.10.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_fail/T10285
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Richard and I uncovered this

{-# LANGUAGE RoleAnnotations #-}
module Bar( N ) where   -- Data constructor not exported

type role N representational
newtype N a = MkN Int

and

{-# LANGUAGE FlexibleContexts #-}
module Foo where

import Data.Coerce
import Data.Type.Coercion
import Bar

f :: Coercible (N a) (N b) => Coercion a b
f = Coercion

This compiles but it should not! It wrongly compiles by using nth (N a ~R N b); but (as Fig 4 of the Corcible paper says), we can't decompose a newtype at representational role.

Easy to fix.

Change History (5)

comment:1 Changed 3 years ago by simonpj

Owner: set to goldfire

comment:2 Changed 3 years ago by simonpj

Also add a check in Lint

comment:3 Changed 3 years ago by Richard Eisenberg <eir@…>

In a8d39a7255df187b742fecc049f0de6528b9acad/ghc:

Fix #10285 by refusing to use NthCo on a newtype.

During this commit, I tested to make sure that CoreLint actually
catches the Core error if the typechecker doesn't.

Test case: typecheck/should_fail/T10285

comment:4 Changed 3 years ago by goldfire

Status: newmerge
Test Case: typecheck/should_fail/T10285

comment:5 Changed 3 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Merged to ghc-7.10.

Note: See TracTickets for help on using tickets.