Commit 518f2895 authored by Edward Z. Yang's avatar Edward Z. Yang

New story for abstract data types in hsig files.

Summary:
In the old implementation of hsig files, we directly
reused the implementation of abstract data types from
hs-boot files.  However, this was WRONG.  Consider the
following program (an abridged version of bkpfail24):

    {-# LANGUAGE GADTs #-}
    unit p where
        signature H1 where
            data T
        signature H2 where
            data T
        module M where
            import qualified H1
            import qualified H2

            f :: H1.T ~ H2.T => a -> b
            f x = x

Prior to this patch, M was accepted, because the type
inference engine concluded that H1.T ~ H2.T does not
hold (indeed, *presently*, it does not).  However, if
we subsequently instantiate p with the same module for
H1 and H2, H1.T ~ H2.T does hold!  Unsound.

The key is that abstract types from signatures need to
be treated like *skolem variables*, since you can interpret
a Backpack unit as a record which is universally quantified
over all of its abstract types, as such (with some fake
syntax for structural records):

    p :: forall t1 t2. { f :: t1 ~ t2 => a -> b }
    p = { f = \x -> x } -- ill-typed

Clearly t1 ~ t2 is not solvable inside p, and also clearly
it could be true at some point in the future, so we better
not treat the lambda expression after f as inaccessible.

The fix seems to be simple: do NOT eagerly fail when trying
to simplify the given constraints.  Instead, treat H1.T ~ H2.T
as an irreducible constraint (rather than an insoluble
one); this causes GHC to treat f as accessible--now we will
typecheck the rest of the function (and correctly fail).
Per the OutsideIn(X) paper, it's always sound to fail less
when simplifying givens.

We do NOT apply this fix to hs-boot files, where abstract
data is also guaranteed to be nominally distinct (since
it can't be implemented via a reexport or a type synonym.)
This is a somewhat unnatural state of affairs (there's
no way to really interpret this in Haskell land) but
no reason to change behavior.

I deleted "representationally distinct abstract data",
which is never used anywhere in GHC.

In the process of constructing this fix, I also realized
our implementation of type synonym matching against abstract
data was not sufficiently restrictive.  In order for
a type synonym T to be well-formed type, it must be a
nullary synonym (i.e., type T :: * -> *, not type T a = ...).
Furthermore, since we use abstract data when defining
instances, they must not have any type family applications.

More details in #12680.  This probably deserves some sort
of short paper report.
Signed-off-by: default avatarEdward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: goldfire, simonpj, austin, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2594
parent a6094fa0
......@@ -9,7 +9,6 @@ module BuildTyCl (
buildDataCon, mkDataConUnivTyVarBinders,
buildPatSyn,
TcMethInfo, buildClass,
distinctAbstractTyConRhs, totallyAbstractTyConRhs,
mkNewTyConRhs, mkDataTyConRhs,
newImplicitBinder, newTyConRepName
) where
......@@ -39,10 +38,6 @@ import UniqSupply
import Util
import Outputable
distinctAbstractTyConRhs, totallyAbstractTyConRhs :: AlgTyConRhs
distinctAbstractTyConRhs = AbstractTyCon True
totallyAbstractTyConRhs = AbstractTyCon False
mkDataTyConRhs :: [DataCon] -> AlgTyConRhs
mkDataTyConRhs cons
= DataTyCon {
......
......@@ -62,7 +62,7 @@ import Fingerprint
import Binary
import BooleanFormula ( BooleanFormula, pprBooleanFormula, isTrue )
import Var( TyVarBndr(..) )
import TyCon ( Role (..), Injectivity(..) )
import TyCon ( Role (..), Injectivity(..), HowAbstract(..) )
import StaticFlags (opt_PprStyle_Debug)
import Util( filterOut, filterByList )
import DataCon (SrcStrictness(..), SrcUnpackedness(..))
......@@ -209,7 +209,7 @@ data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr]
-- See Note [Storing compatibility] in CoAxiom
data IfaceConDecls
= IfAbstractTyCon Bool -- c.f TyCon.AbstractTyCon
= IfAbstractTyCon HowAbstract -- c.f TyCon.AbstractTyCon
| IfDataTyCon [IfaceConDecl] Bool [FieldLabelString] -- Data type decls
| IfNewTyCon IfaceConDecl Bool [FieldLabelString] -- Newtype decls
......@@ -697,7 +697,10 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype,
fls = ifaceConDeclFields condecls
pp_nd = case condecls of
IfAbstractTyCon d -> text "abstract" <> ppShowIface ss (parens (ppr d))
IfAbstractTyCon how ->
case how of
DistinctNominalAbstract -> text "abstract"
SkolemAbstract -> text "skolem"
IfDataTyCon{} -> text "data"
IfNewTyCon{} -> text "newtype"
......
......@@ -924,6 +924,11 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
; stopWith ev "Decomposed TyConApp" }
else canEqFailure ev eq_rel ty1 ty2 }
-- See Note [Skolem abstract data] (at SkolemAbstract)
| isSkolemAbstractTyCon tc1 || isSkolemAbstractTyCon tc2
= do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
; continueWith (CIrredEvCan { cc_ev = ev }) }
-- Fail straight away for better error messages
-- See Note [Use canEqFailure in canDecomposableTyConApp]
| eq_rel == ReprEq && not (isGenerativeTyCon tc1 Representational &&
......
......@@ -956,10 +956,41 @@ checkBootTyCon is_boot tc1 tc2
check (roles1 == roles2) roles_msg `andThenCheck`
check (eqTypeX env syn_rhs1 syn_rhs2) empty -- nothing interesting to say
-- Type synonyms for hs-boot are questionable, so they
-- are not supported at the moment
| not is_boot && isAbstractTyCon tc1 && isTypeSynonymTyCon tc2
= check (roles1 == roles2) roles_msg
-- A skolem abstract TyCon can be implemented using a type synonym, but ONLY
-- if the type synonym is nullary and has no type family applications.
-- This arises from two properties of skolem abstract data:
--
-- For any T (with some number of paramaters),
--
-- 1. T is a valid type (it is "curryable"), and
--
-- 2. T is valid in an instance head (no type families).
--
-- See also 'HowAbstract' and Note [Skolem abstract data].
--
| isSkolemAbstractTyCon tc1
, Just (tvs, ty) <- synTyConDefn_maybe tc2
, Just (tc2', args) <- tcSplitTyConApp_maybe ty
= check (null (tcTyFamInsts ty))
(text "Illegal type family application in implementation of abstract data.")
`andThenCheck`
check (null tvs)
(text "Illegal parameterized type synonym in implementation of abstract data." $$
text "(Try eta reducing your type synonym so that it is nullary.)")
`andThenCheck`
-- Don't report roles errors unless the type synonym is nullary
checkUnless (not (null tvs)) $
ASSERT ( null roles2 )
-- If we have something like:
--
-- signature H where
-- data T a
-- module H where
-- data K a b = ...
-- type T = K Int
--
-- we need to drop the first role of K when comparing!
check (roles1 == drop (length args) (tyConRoles tc2')) roles_msg
| Just fam_flav1 <- famTyConFlav_maybe tc1
, Just fam_flav2 <- famTyConFlav_maybe tc2
......@@ -997,11 +1028,8 @@ checkBootTyCon is_boot tc1 tc2
(text "Roles on abstract types default to" <+>
quotes (text "representational") <+> text "in boot files.")
eqAlgRhs tc (AbstractTyCon dis1) rhs2
| dis1 = check (isGenInjAlgRhs rhs2) --Check compatibility
(text "The natures of the declarations for" <+>
quotes (ppr tc) <+> text "are different")
| otherwise = checkSuccess
eqAlgRhs _ (AbstractTyCon _) _rhs2
= checkSuccess -- rhs2 is guaranteed to be injective, since it's an AlgTyCon
eqAlgRhs _ tc1@DataTyCon{} tc2@DataTyCon{} =
checkListBy eqCon (data_cons tc1) (data_cons tc2) (text "constructors")
eqAlgRhs _ tc1@NewTyCon{} tc2@NewTyCon{} =
......
......@@ -1427,7 +1427,7 @@ isPartialSig _ = False
************************************************************************
-}
-- The syntax of xi types:
-- The syntax of xi (ξ) types:
-- xi ::= a | T xis | xis -> xis | ... | forall a. tau
-- Two important notes:
-- (i) No type families, unless we are under a ForAll
......
......@@ -932,7 +932,8 @@ tcDataDefn roles_info
; stupid_theta <- zonkTcTypeToTypes emptyZonkEnv
stupid_tc_theta
; kind_signatures <- xoptM LangExt.KindSignatures
; is_boot <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
; tcg_env <- getGblEnv
; let hsc_src = tcg_src tcg_env
-- Check that we don't use kind signatures without Glasgow extensions
; when (isJust mb_ksig) $
......@@ -943,7 +944,7 @@ tcDataDefn roles_info
; tycon <- fixM $ \ tycon -> do
{ let res_ty = mkTyConApp tycon (mkTyVarTys (binderVars final_bndrs))
; data_cons <- tcConDecls tycon (final_bndrs, res_ty) cons
; tc_rhs <- mk_tc_rhs is_boot tycon data_cons
; tc_rhs <- mk_tc_rhs hsc_src tycon data_cons
; tc_rep_nm <- newTyConRepName tc_name
; return (mkAlgTyCon tc_name
final_bndrs
......@@ -956,10 +957,18 @@ tcDataDefn roles_info
; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs)
; return tycon }
where
mk_tc_rhs is_boot tycon data_cons
| null data_cons, is_boot -- In a hs-boot file, empty cons means
= return totallyAbstractTyConRhs -- "don't know"; hence totally Abstract
| otherwise
-- In hs-boot, a 'data' declaration with no constructors
-- indicates an nominally distinct abstract data type.
mk_tc_rhs HsBootFile _ []
= return (AbstractTyCon DistinctNominalAbstract)
-- In hsig, a 'data' declaration indicates a skolem
-- abstract data type. See 'HowAbstract' and Note
-- [Skolem abstract data] for more commentary.
mk_tc_rhs HsigFile _ []
= return (AbstractTyCon SkolemAbstract)
mk_tc_rhs _ tycon data_cons
= case new_or_data of
DataType -> return (mkDataTyConRhs data_cons)
NewType -> ASSERT( not (null data_cons) )
......
......@@ -10,7 +10,7 @@ The @TyCon@ datatype
module TyCon(
-- * Main TyCon data types
TyCon, AlgTyConRhs(..), visibleDataCons,
TyCon, AlgTyConRhs(..), HowAbstract(..), visibleDataCons,
AlgTyConFlav(..), isNoParent,
FamTyConFlav(..), Role(..), Injectivity(..),
RuntimeRepInfo(..),
......@@ -55,6 +55,7 @@ module TyCon(
isDataSumTyCon_maybe,
isEnumerationTyCon,
isNewTyCon, isAbstractTyCon,
isSkolemAbstractTyCon,
isFamilyTyCon, isOpenFamilyTyCon,
isTypeFamilyTyCon, isDataFamilyTyCon,
isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
......@@ -721,7 +722,6 @@ data TyCon
-- tycon's body. See Note [TcTyCon]
}
-- | Represents right-hand-sides of 'TyCon's for algebraic types
data AlgTyConRhs
......@@ -729,9 +729,7 @@ data AlgTyConRhs
-- it's represented by a pointer. Used when we export a data type
-- abstractly into an .hi file.
= AbstractTyCon
Bool -- True <=> It's definitely a distinct data type,
-- equal only to itself; ie not a newtype
-- False <=> Not sure
HowAbstract
-- | Information about those 'TyCon's derived from a @data@
-- declaration. This includes data types with no constructors at
......@@ -789,6 +787,72 @@ data AlgTyConRhs
-- again check Trac #1072.
}
-- | An 'AbstractTyCon' represents some matchable type constructor (i.e., valid
-- in instance heads), for which we do not know the implementation. We refer to
-- these as "abstract data".
--
-- At the moment, there are two flavors of abstract data, corresponding
-- to whether or not the abstract data declaration occurred in an hs-boot
-- file or an hsig file.
--
data HowAbstract
-- | Nominally distinct abstract data arises from abstract data
-- declarations in an hs-boot file.
--
-- Abstract data of this form is guaranteed to be nominally distinct
-- from all other declarations in the system; e.g., if I have
-- a @data T@ and @data S@ in an hs-boot file, it is safe to
-- assume that they will never equal each other. This is something
-- of an implementation accident: it is a lot easier to assume that
-- @data T@ in @A.hs-boot@ indicates there will be @data T = ...@
-- in @A.hs@, than to permit the possibility that @A.hs@ reexports
-- it from somewhere else.
= DistinctNominalAbstract
-- Note [Skolem abstract data]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Skolem abstract data arises from abstract data declarations
-- in an hsig file.
--
-- The best analogy is to interpret the abstract types in Backpack
-- unit as elaborating to universally quantified type variables;
-- e.g.,
--
-- unit p where
-- signature H where
-- data T
-- data S
-- module M where
-- import H
-- f :: (T ~ S) => a -> b
-- f x = x
--
-- elaborates as (with some fake structural types):
--
-- p :: forall t s. { f :: forall a b. t ~ s => a -> b }
-- p = { f = \x -> x } -- ill-typed
--
-- It is clear that inside p, t ~ s is not provable (and
-- if we tried to write a function to cast t to s, that
-- would not work), but if we call p @Int @Int, clearly Int ~ Int
-- is provable. The skolem variables are all distinct from
-- one another, but we can't make assumptions like "f is
-- inaccessible", because the skolem variables will get
-- instantiated eventually!
--
-- Skolem abstract data still has the constraint that there
-- are no type family applications, to keep this data matchable.
| SkolemAbstract
instance Binary HowAbstract where
put_ bh DistinctNominalAbstract = putByte bh 0
put_ bh SkolemAbstract = putByte bh 1
get bh = do { h <- getByte bh
; case h of
0 -> return DistinctNominalAbstract
_ -> return SkolemAbstract }
-- | Some promoted datacons signify extra info relevant to GHC. For example,
-- the @IntRep@ constructor of @RuntimeRep@ corresponds to the 'IntRep'
-- constructor of 'PrimRep'. This data structure allows us to store this
......@@ -1543,6 +1607,12 @@ isAbstractTyCon :: TyCon -> Bool
isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon {} }) = True
isAbstractTyCon _ = False
-- | Test if the 'TyCon' is totally abstract; i.e., it is not even certain
-- to be nominally distinct.
isSkolemAbstractTyCon :: TyCon -> Bool
isSkolemAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon SkolemAbstract }) = True
isSkolemAbstractTyCon _ = False
-- | Make an fake, abstract 'TyCon' from an existing one.
-- Used when recovering from errors
makeTyConAbstract :: TyCon -> TyCon
......@@ -1640,7 +1710,7 @@ isGenInjAlgRhs :: AlgTyConRhs -> Bool
isGenInjAlgRhs (TupleTyCon {}) = True
isGenInjAlgRhs (SumTyCon {}) = True
isGenInjAlgRhs (DataTyCon {}) = True
isGenInjAlgRhs (AbstractTyCon distinct) = distinct
isGenInjAlgRhs (AbstractTyCon {}) = False
isGenInjAlgRhs (NewTyCon {}) = False
-- | Is this 'TyCon' that for a @newtype@
......
......@@ -29,3 +29,5 @@ test('bkp34', normal, backpack_compile, [''])
# instance merging when heads overlap prefers an arbitrary instance
test('bkp35', expect_broken(0), backpack_compile, [''])
test('bkp36', normal, backpack_compile, [''])
test('bkp37', normal, backpack_compile, [''])
test('bkp38', normal, backpack_compile, [''])
{-# LANGUAGE FlexibleInstances #-}
unit p where
signature A where
data K a
instance Show (K Int)
instance Show (K Bool)
unit q where
module A where
type K = []
unit r where
dependency p[A=q:A]
[1 of 3] Processing p
[1 of 1] Compiling A[sig] ( p/A.hsig, nothing )
[2 of 3] Processing q
Instantiating q
[1 of 1] Compiling A ( q/A.hs, bkp37.out/q/A.o )
[3 of 3] Processing r
Instantiating r
[1 of 1] Including p[A=q:A]
Instantiating p[A=q:A]
[1 of 1] Compiling A[sig] ( p/A.hsig, bkp37.out/p/p-HVmFlcYSefiK5n1aDP1v7x/A.o )
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RoleAnnotations #-}
unit p where
signature A where
type role K nominal
data K a
instance Show (K Int)
instance Show (K Bool)
unit q where
module A where
type role T representational nominal
data T a b = MkT
deriving (Show)
type K = T ()
unit r where
dependency p[A=q:A]
[1 of 3] Processing p
[1 of 1] Compiling A[sig] ( p/A.hsig, nothing )
[2 of 3] Processing q
Instantiating q
[1 of 1] Compiling A ( q/A.hs, bkp38.out/q/A.o )
[3 of 3] Processing r
Instantiating r
[1 of 1] Including p[A=q:A]
Instantiating p[A=q:A]
[1 of 1] Compiling A[sig] ( p/A.hsig, bkp38.out/p/p-HVmFlcYSefiK5n1aDP1v7x/A.o )
......@@ -19,3 +19,8 @@ test('bkpfail20', normal, backpack_compile_fail, [''])
test('bkpfail21', normal, backpack_compile_fail, [''])
# it does fail, but not quite in the right way yet...
test('bkpfail22', expect_broken(0), backpack_compile_fail, [''])
test('bkpfail23', normal, backpack_compile_fail, [''])
test('bkpfail24', normal, backpack_compile_fail, [''])
test('bkpfail25', normal, backpack_compile_fail, [''])
test('bkpfail26', normal, backpack_compile_fail, [''])
test('bkpfail27', normal, backpack_compile_fail, [''])
......@@ -13,7 +13,7 @@ bkpfail10.bkp:8:9: error:
Type constructor ‘q:H.H’ has conflicting definitions in the module
and its hsig file
Main module: data q:H.H a = q:H.H a
Hsig file: abstract q:H.H
Hsig file: skolem q:H.H
The types have different kinds
bkpfail10.bkp:10:9: error:
......
{-# LANGUAGE GADTs, RoleAnnotations #-}
unit p where
signature H where
type role F phantom
data F a
module M where
import H
-- This will typecheck
f :: (F a ~ F b) => a -> b
f x = x
unit h where
module H where
-- But this is an invalid implementation of F
type F a = ()
unit r where
dependency p[H=h:H]
[1 of 3] Processing p
[1 of 2] Compiling H[sig] ( p/H.hsig, nothing )
[2 of 2] Compiling M ( p/M.hs, nothing )
[2 of 3] Processing h
Instantiating h
[1 of 1] Compiling H ( h/H.hs, bkpfail23.out/h/H.o )
[3 of 3] Processing r
Instantiating r
[1 of 1] Including p[H=h:H]
Instantiating p[H=h:H]
[1 of 2] Compiling H[sig] ( p/H.hsig, bkpfail23.out/p/p-6KeuBvYi0jvLWqVbkSAZMq/H.o )
bkpfail23.bkp:14:9: error:
Type constructor ‘h:H.F’ has conflicting definitions in the module
and its hsig file
Main module: type h:H.F a = ()
Hsig file: type role h:H.F phantom
skolem h:H.F a
Illegal parameterized type synonym in implementation of abstract data.
(Try eta reducing your type synonym so that it is nullary.)
{-# LANGUAGE GADTs #-}
unit p where
signature H1 where
data T
signature H2 where
data T
module M where
import qualified H1
import qualified H2
-- This is NOT an insoluble given, so we
-- should complain a doesn't match b
f :: H1.T ~ H2.T => a -> b
f x = x
-- This equality does NOT hold, we should
-- complain that H1.T doesn't match H2.T
g :: H1.T -> H2.T
g x = x
[1 of 1] Processing p
[1 of 3] Compiling H1[sig] ( p/H1.hsig, nothing )
[2 of 3] Compiling H2[sig] ( p/H2.hsig, nothing )
[3 of 3] Compiling M ( p/M.hs, nothing )
bkpfail24.bkp:14:15: error:
• Could not deduce: a ~ b
from the context: {H1.T} ~ {H2.T}
bound by the type signature for:
f :: {H1.T} ~ {H2.T} => a -> b
at bkpfail24.bkp:13:9-34
‘a’ is a rigid type variable bound by
the type signature for:
f :: forall a b. {H1.T} ~ {H2.T} => a -> b
at bkpfail24.bkp:13:9-34
‘b’ is a rigid type variable bound by
the type signature for:
f :: forall a b. {H1.T} ~ {H2.T} => a -> b
at bkpfail24.bkp:13:9-34
• In the expression: x
In an equation for ‘f’: f x = x
• Relevant bindings include
x :: a (bound at bkpfail24.bkp:14:11)
f :: a -> b (bound at bkpfail24.bkp:14:9)
bkpfail24.bkp:19:15: error:
• Couldn't match expected type ‘{H2.T}’
with actual type ‘{H1.T}’
NB: ‘{H1.T}’ is defined at bkpfail24.bkp:4:9-14
‘{H2.T}’ is defined at bkpfail24.bkp:6:9-14
• In the expression: x
In an equation for ‘g’: g x = x
{-# LANGUAGE TypeSynonymInstances #-}
unit p where
signature H where
data T a
module M where
import H
instance Functor T
unit q where
module H where
-- No good!
type T a = a
unit r where
dependency p[H=q:H]
{-
If we get:
The type synonym ‘T’ should have 1 argument, but has been given none
In the instance declaration for ‘Functor T’
that is too late! Need to catch this earlier.
-}
[1 of 3] Processing p
[1 of 2] Compiling H[sig] ( p/H.hsig, nothing )
[2 of 2] Compiling M ( p/M.hs, nothing )
bkpfail25.bkp:7:18: warning: [-Wmissing-methods (in -Wdefault)]
• No explicit implementation for
‘fmap’
• In the instance declaration for ‘Functor T’
[2 of 3] Processing q
Instantiating q
[1 of 1] Compiling H ( q/H.hs, bkpfail25.out/q/H.o )
[3 of 3] Processing r
Instantiating r
[1 of 1] Including p[H=q:H]
Instantiating p[H=q:H]
[1 of 2] Compiling H[sig] ( p/H.hsig, bkpfail25.out/p/p-D5Mg3foBSCrDbQDKH4WGSG/H.o )
bkpfail25.bkp:12:9: error:
Type constructor ‘q:H.T’ has conflicting definitions in the module
and its hsig file
Main module: type q:H.T a = a
Hsig file: skolem q:H.T a
{-# LANGUAGE TypeSynonymInstances #-}
unit p where
signature H where
data T a
module M where
import H
instance Functor T where
fmap = undefined
unit q where
module H where
-- The type synonym is not eta reduced, so we reject it.
-- This test will start passing if GHC automatically eta
-- reduces type synonyms when it can, see #12701
type T a = [a]
unit r where
dependency p[H=q:H]
[1 of 3] Processing p
[1 of 2] Compiling H[sig] ( p/H.hsig, nothing )
[2 of 2] Compiling M ( p/M.hs, nothing )
[2 of 3] Processing q
Instantiating q
[1 of 1] Compiling H ( q/H.hs, bkpfail26.out/q/H.o )
[3 of 3] Processing r
Instantiating r
[1 of 1] Including p[H=q:H]
Instantiating p[H=q:H]
[1 of 2] Compiling H[sig] ( p/H.hsig, bkpfail26.out/p/p-D5Mg3foBSCrDbQDKH4WGSG/H.o )
bkpfail26.bkp:15:9: error:
Type constructor ‘q:H.T’ has conflicting definitions in the module
and its hsig file
Main module: type q:H.T a = [a]
Hsig file: skolem q:H.T a
Illegal parameterized type synonym in implementation of abstract data.
(Try eta reducing your type synonym so that it is nullary.)
{-# LANGUAGE TypeFamilies #-}
unit p where
signature H where
data T
module M where
import H
instance Show T where
show = undefined
unit q where
module H where
-- Illegal type family!
type family F
type instance F = Bool
type T = F
unit r where
dependency p[H=q:H]
[1 of 3] Processing p
[1 of 2] Compiling H[sig] ( p/H.hsig, nothing )
[2 of 2] Compiling M ( p/M.hs, nothing )
[2 of 3] Processing q
Instantiating q
[1 of 1] Compiling H ( q/H.hs, bkpfail27.out/q/H.o )
[3 of 3] Processing r
Instantiating r
[1 of 1] Including p[H=q:H]
Instantiating p[H=q:H]
[1 of 2] Compiling H[sig] ( p/H.hsig, bkpfail27.out/p/p-D5Mg3foBSCrDbQDKH4WGSG/H.o )
bkpfail27.bkp:15:9: error:
Type constructor ‘q:H.T’ has conflicting definitions in the module
and its hsig file
Main module: type q:H.T = q:H.F
Hsig file: skolem q:H.T
Illegal type family application in implementation of abstract data.
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