Opened 5 years ago

Closed 5 years ago

Last modified 5 years ago

#9580 closed bug (fixed)

Possible excessive leniency in interaction between coerce and data families?

Reported by: dmcclean Owned by: simonpj
Priority: low Milestone:
Component: Compiler (Type checker) Version: 7.8.3
Keywords: Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed-types/should_fail/T9580
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Per goldfire's request at #8177, I am promoting this issue into it's own ticket. I am entirely not confident that it represents a bug; I raise the issue because, while it happens to do exactly what I want, I cannot understand *why* it does what I want, and it seems like it might possibly also do related undesirable things.

I have the following situation, which I have distilled from a real use case, retaining its identifiers but eliding a whole bunch of irrelevant detail. The real thing is on GitHub if it helps anyone to see why I want to do this, but it's really a side issue AFAICT.

It's split into two modules, because goldfire had suggested that it might have arisen because the newtype constructor Quantity' was in scope at the site of the coerce, this test shows that it arises even when Quantity' is not in scope.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}

module Test
(
  Quantity, Unit,
  Dimension(..),
  Variant(..),
  Mass,
  KnownVariant(Dimensional)
)
where

data Variant = DQuantity | DUnit

data Dimension = DMass | DLength | DTime -- ... this isn't the real way, it's simplified

data UnitName = UnitName String

class KnownVariant (var :: Variant) where
  data Dimensional var :: Dimension -> * -> *

instance KnownVariant DQuantity where
  newtype Dimensional DQuantity d v = Quantity' v

instance KnownVariant DUnit where
  data Dimensional DUnit d v = Unit' UnitName v

instance (Show v) => Show (Dimensional DQuantity d v) where
  show (Quantity' x) = "As A Quantity " ++ show x

type Quantity = Dimensional DQuantity

type Unit = Dimensional DUnit

type Mass v = Quantity DMass v

And the main module:

module Main where

import Test
import Data.Coerce

main = do
         let x = 3.7 :: Double
         putStrLn . show $ x
         let y = (coerce x) :: Mass Double
         putStrLn . show $ y
         let z = (coerce y) :: Double
         putStrLn . show $ z

My question is in two parts:

1) Why are these coercions allowed if the role signature of Dimensional is, as GHCi's :i tells me, nominal nominal nominal?

2) Is this the intended behavior?

Change History (10)

comment:1 Changed 5 years ago by dmcclean

I tried a bunch of variations to see if I could get this to not compile to see what might be causing it. It still works if you move the type synonym definitions of Mass and Quantity out of Test and into Main (as long as you move the language extensions too).

It still works even if the last type parameter is held polymorphic, as

f :: Num v => v -> Mass v
f x = coerce $ 3 * x

even when f is defined in Main.

It even still works if the last two parameters are held polymorphic, as

g :: Num v => v -> Quantity d v
g x = coerce $ 3 * x

even when g is defined in Main.

It also works if you do the same thing but expand the type synonyms manually.

comment:2 Changed 5 years ago by simonpj

Oh yes, this is a real bug. Here is a cut-down test case

{-# LANGUAGE KindSignatures, TypeFamilies #-}
module T9580a( Dimensional ) where

data family Dimensional var :: * -> *
newtype instance Dimensional Int v = Quantity' v

------------------

module T9680 where

import T9580a
import Data.Coerce

foo :: Dimensional Int Double -> Double
foo x = coerce x

Obviously, the latter module should fail to type check, since Quantity' is not in scope.

Simon

comment:3 Changed 5 years ago by simonpj

Owner: set to simonpj

I'm on this (refactoring...), but am now out of action till Tues.

SImon

comment:4 Changed 5 years ago by Simon Peyton Jones <simonpj@…>

In 0aaf812ed0a4a4be9528b2e2f6b72bee7cd8002d/ghc:

Clean up Coercible handling, and interaction of data families with newtypes

This patch fixes Trac #9580, in which the Coercible machinery succeeded
even though the relevant data constructor was not in scope.

As usual I got dragged into a raft of refactoring changes,
all for the better.

* Delete TcEvidence.coercionToTcCoercion (now unused)

* Move instNewTyConTF_maybe, instNewTyCon_maybe to FamInst,
  and rename them to tcInstNewTyConTF_maybe, tcInstNewTyCon
  (They both return TcCoercions.)

* tcInstNewTyConTF_maybe also gets more convenient type,
  which improves TcInteract.getCoercibleInst

* Define FamInst.tcLookupDataFamInst, and use it in TcDeriv,
  (as well as in tcInstNewTyConTF_maybe)

* Improve error report for Coercible errors, when data familes
  are involved  Another use of tcLookupDataFamInst

* In TcExpr.tcTagToEnum, use tcLookupDataFamInst to replace
  local hacky code

* Fix Coercion.instNewTyCon_maybe and Type.newTyConInstRhs to deal
  with eta-reduced newtypes, using
  (new) Type.unwrapNewTyConEtad_maybe and (new) Type.applyTysX

Some small refactoring of TcSMonad.matchFam.

comment:5 Changed 5 years ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_fail/T9580

Thank you for identifying this.

Simon

comment:6 Changed 5 years ago by dmcclean

Thanks for fixing it!

I just have one followup question. One reason the coercion shouldn't have worked is because the newtype constructor wasn't in scope.

But, with the newtype constructor in scope, should it be coercible or not? I thought that it should still not be, because the data family's role signature has all nominal arguments. The newtype instance happens to use its argument in a representational way, but should that property of the definition be visible when "looking through" the data family?

(It may be the case that one of your refactoring changes addresses this, I don't understand most of those comments.)

comment:7 Changed 5 years ago by simonpj

Cam you give a concrete example? And compare with whatever the paper says?

comment:8 Changed 5 years ago by dmcclean

I think I may have been confused for 2 different reasons.

First, I forgot that we are coercing in your example from Dimensional Int Double -> Double, which should work according to rule 2 in figure 2. I had it mixed up with converting from Dimensional Int Double -> Dimensional Int x (where there is a coercion from Double to x).

Second, it doesn't appear to actually be possible to export the Quantity' constructor from the defining module at all. (If I put it in the export list, GHCi tells me that it isn't in scope even though it is and I checked the spelling three times.) So the scenario I was thinking of isn't possible for that reason too; I hadn't realized that this was a rule.

I now think that with the change you made everything is correct, sorry for the confusion.

comment:9 in reply to:  8 Changed 5 years ago by dfeuer

Replying to dmcclean:

I think I may have been confused for 2 different reasons.

First, I forgot that we are coercing in your example from Dimensional Int Double -> Double, which should work according to rule 2 in figure 2. I had it mixed up with converting from Dimensional Int Double -> Dimensional Int x (where there is a coercion from Double to x).

Second, it doesn't appear to actually be possible to export the Quantity' constructor from the defining module at all. (If I put it in the export list, GHCi tells me that it isn't in scope even though it is and I checked the spelling three times.) So the scenario I was thinking of isn't possible for that reason too; I hadn't realized that this was a rule.

I now think that with the change you made everything is correct, sorry for the confusion.

Did you use the proper export syntax, Dimensional (Quantity')? That's supposed to work. If you didn't get an unknown whatever error when exporting Quantity' from the defining module, I'm guessing that it exported the Quantity' type (produced by DataKinds) rather than the data constructor. I don't really know how that extension is supposed to work with module exports though.

comment:10 Changed 5 years ago by dmcclean

No, I did not use the proper export syntax. I'm sorry, I wasn't aware of it. With the proper syntax it does work.

Thank you both again.

Note: See TracTickets for help on using tickets.