Commit ace8d4fc authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Fix #10493.

Now, a Coercible (T1 ...) (T2 ...) constraint is insoluble only
when both T1 and T2 say "yes" to isDistinctTyCon. Several comments
also updated in this patch.
parent 0de0b146
......@@ -665,7 +665,7 @@ canDecomposableTyConApp ev eq_rel tc1 tys1 tc2 tys2
-- Fail straight away for better error messages
-- See Note [Use canEqFailure in canDecomposableTyConApp]
| isDataFamilyTyCon tc1 || isDataFamilyTyCon tc2
| eq_rel == ReprEq && not (isDistinctTyCon tc1 && isDistinctTyCon tc2)
= canEqFailure ev eq_rel ty1 ty2
| otherwise
= canEqHardFailure ev eq_rel ty1 ty2
......@@ -678,7 +678,7 @@ Note [Use canEqFailure in canDecomposableTyConApp]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We must use canEqFailure, not canEqHardFailure here, because there is
the possibility of success if working with a representational equality.
Here is the case:
Here is one case:
type family TF a where TF Char = Bool
data family DF a
......@@ -688,6 +688,13 @@ Suppose we are canonicalising (Int ~R DF (T a)), where we don't yet
know `a`. This is *not* a hard failure, because we might soon learn
that `a` is, in fact, Char, and then the equality succeeds.
Here is another case:
[G] Coercible Age Int
where Age's constructor is not in scope. We don't want to report
an "inaccessible code" error in the context of this Given!
Note [Decomposing newtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
As explained in Note [NthCo and newtypes] in Coercion, we can't use
......
......@@ -1211,7 +1211,7 @@ isDataTyCon (AlgTyCon {algTcRhs = rhs})
isDataTyCon _ = False
-- | 'isDistinctTyCon' is true of 'TyCon's that are equal only to
-- themselves, even via coercions (except for unsafeCoerce).
-- themselves, even via representational coercions (except for unsafeCoerce).
-- This excludes newtypes, type functions, type synonyms.
-- It relates directly to the FC consistency story:
-- If the axioms are consistent,
......
......@@ -280,8 +280,8 @@ to 'Bool', in which case x::T Int, so
Suppose x::T X. Then *in Haskell* it's impossible to construct a (non-bottom)
value of type (T X) using T1. But *in FC* it's quite possible. The newtype
gives a coercion
CoX :: X ~ Int
So (T CoX) :: T X ~ T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
CoX :: X ~R Int
So (T CoX)_R :: T X ~R T Int; hence (T1 `cast` sym (T CoX)) is a non-bottom value
of type (T X) constructed with T1. Hence
ANSWER = NO we can't prune the T1 branch (surprisingly)
......@@ -317,6 +317,13 @@ drop more and more dead code.
For now we implement a very simple test: type variables match
anything, type functions (incl newtypes) match anything, and only
distinct data types fail to match. We can elaborate later.
NB: typesCantMatch is subtly different than the apartness checks
elsewhere in this module. It reasons over *representational* equality
(saying that a newtype is not distinct from its representation) whereas
the checks in, say, tcUnifyTysFG are about *nominal* equality. tcUnifyTysFG
also assumes that its inputs are type-family-free, whereas no such assumption
is in play here.
-}
typesCantMatch :: [(Type,Type)] -> Bool
......
{-# LANGUAGE FlexibleContexts #-}
module T10493 where
import Data.Coerce
import Data.Ord (Down) -- no constructor
foo :: Coercible (Down Int) Int => Down Int -> Int
foo = coerce
......@@ -460,3 +460,4 @@ test('T10423', normal, compile, [''])
test('T10489', normal, compile, [''])
test('T10348', normal, compile, [''])
test('T10494', normal, compile, [''])
test('T10493', normal, compile, [''])
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment