Commit 1eec1f21 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Another major constraint-solver refactoring

This patch takes further my refactoring of the constraint
solver, which I've been doing over the last couple of months
in consultation with Richard.

It fixes a number of tricky bugs that made the constraint
solver actually go into a loop, including

  Trac #12526
  Trac #12444
  Trac #12538

The main changes are these

* Flatten unification variables (fmvs/fuvs) appear on the LHS
  of a tvar/tyvar equality; thus
           fmv ~ alpha
  and not
           alpha ~ fmv

  See Note [Put flatten unification variables on the left]
  in TcUnify.  This is implemented by TcUnify.swapOverTyVars.

* Don't reduce a "loopy" CFunEqCan where the fsk appears on
  the LHS:
      F t1 .. tn ~ fsk
  where 'fsk' is free in t1..tn.
  See Note [FunEq occurs-check principle] in TcInteract

  This neatly stops some infinite loops that people reported;
  and it allows us to delete some crufty code in reduce_top_fun_eq.
  And it appears to be no loss whatsoever.

  As well as fixing loops, ContextStack2 and T5837 both terminate
  when they didn't before.

* Previously we generated "derived shadow" constraints from
  Wanteds, but we could (and sometimes did; Trac #xxxx) repeatedly
  generate a derived shadow from the same Wanted.

  A big change in this patch is to have two kinds of Wanteds:
     [WD] behaves like a pair of a Wanted and a Derived
     [W]  behaves like a Wanted only
  See CtFlavour and ShadowInfo in TcRnTypes, and the ctev_nosh
  field of a Wanted.

  This turned out to be a lot simpler.  A [WD] gets split into a
  [W] and a [D] in TcSMonad.maybeEmitShaodow.

  See TcSMonad Note [The improvement story and derived shadows]

* Rather than have a separate inert_model in the InertCans, I've
  put the derived equalities back into inert_eqs.  We weren't
  gaining anything from a separate field.

* Previously we had a mode for the constraint solver in which it
  would more aggressively solve Derived constraints; it was used
  for simplifying the context of a 'deriving' clause, or a 'default'
  delcaration, for example.

  But the complexity wasn't worth it; now I just make proper Wanted
  constraints.  See TcMType.cloneWC

* Don't generate injectivity improvement for Givens; see
  Note [No FunEq improvement for Givens] in TcInteract

* solveSimpleWanteds leaves the insolubles in-place rather than
  returning them.  Simpler.

I also did lots of work on comments, including fixing Trac #12821.
parent 0123efde
......@@ -107,6 +107,8 @@ toIfaceKind = toIfaceType
toIfaceType :: Type -> IfaceType
-- Synonyms are retained in the interface type
toIfaceType (TyVarTy tv) = IfaceTyVar (toIfaceTyVar tv)
-- | isTcTyVar tv = IfaceTyVar (toIfaceTyVar tv `appendFS` consFS '_' (mkFastString (showSDocUnsafe (ppr (getUnique tv)))))
-- | otherwise
toIfaceType (AppTy t1 t2) = IfaceAppTy (toIfaceType t1) (toIfaceType t2)
toIfaceType (LitTy n) = IfaceLitTy (toIfaceTyLit n)
toIfaceType (ForAllTy b t) = IfaceForAllTy (toIfaceForAllBndr b) (toIfaceType t)
......
......@@ -3,7 +3,7 @@
module TcCanonical(
canonicalize,
unifyDerived,
makeSuperClasses,
makeSuperClasses, maybeSym,
StopOrContinue(..), stopWith, continueWith
) where
......
......@@ -2682,13 +2682,14 @@ relevantBindings want_filtering ctxt ct
-- et really should be filled in by now. But there's a chance
-- it hasn't, if, say, we're reporting a kind error en route to
-- checking a term. See test indexed-types/should_fail/T8129
; ty <- case mb_ty of
Just ty -> return ty
Nothing -> do { traceTc "Defaulting an ExpType in relevantBindings"
(ppr et)
; expTypeToType et }
; go2 name ty top_lvl }
-- Or we are reporting errors from the ambiguity check on
-- a local type signature
; case mb_ty of
Just ty -> go2 name ty top_lvl
Nothing -> discard_it -- No info; discard
}
where
discard_it = go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
go2 id_name id_type top_lvl
= do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env id_type
; traceTc "relevantBindings 1" (ppr id_name <+> dcolon <+> ppr tidy_ty)
......@@ -2702,17 +2703,19 @@ relevantBindings want_filtering ctxt ct
&& id_tvs `disjointVarSet` ct_tvs)
-- We want to filter out this binding anyway
-- so discard it silently
then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
then discard_it
else if isTopLevel top_lvl && not (isNothing n_left)
-- It's a top-level binding and we have not specified
-- -fno-max-relevant-bindings, so discard it silently
then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
then discard_it
else if run_out n_left && id_tvs `subVarSet` tvs_seen
-- We've run out of n_left fuel and this binding only
-- mentions aleady-seen type variables, so discard it
then go tidy_env ct_tvs n_left tvs_seen docs True tc_bndrs
then go tidy_env ct_tvs n_left tvs_seen docs
True -- Record that we have now discarded something
tc_bndrs
-- Keep this binding, decrement fuel
else go tidy_env' ct_tvs (dec_max n_left) new_seen (doc:docs) discards tc_bndrs }
......
......@@ -1669,6 +1669,7 @@ tcUnboundId unbound res_ty
; loc <- getCtLocM HoleOrigin Nothing
; let can = CHoleCan { cc_ev = CtWanted { ctev_pred = ty
, ctev_dest = EvVarDest ev
, ctev_nosh = WDeriv
, ctev_loc = loc}
, cc_hole = ExprHole unbound }
; emitInsoluble can
......
This diff is collapsed.
This diff is collapsed.
......@@ -43,7 +43,7 @@ module TcMType (
--------------------------------
-- Creating new evidence variables
newEvVar, newEvVars, newDict,
newWanted, newWanteds,
newWanted, newWanteds, cloneWanted, cloneWC,
emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
newTcEvBinds, addTcEvBind,
......@@ -170,11 +170,30 @@ newWanted orig t_or_k pty
else EvVarDest <$> newEvVar pty
return $ CtWanted { ctev_dest = d
, ctev_pred = pty
, ctev_nosh = WDeriv
, ctev_loc = loc }
newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
newWanteds orig = mapM (newWanted orig Nothing)
cloneWanted :: Ct -> TcM CtEvidence
cloneWanted ct
= newWanted (ctEvOrigin ev) Nothing (ctEvPred ev)
where
ev = ctEvidence ct
cloneWC :: WantedConstraints -> TcM WantedConstraints
cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
= do { simples' <- mapBagM clone_one simples
; implics' <- mapBagM clone_implic implics
; return (wc { wc_simple = simples', wc_impl = implics' }) }
where
clone_one ct = do { ev <- cloneWanted ct; return (mkNonCanonical ev) }
clone_implic implic@(Implic { ic_wanted = inner_wanted })
= do { inner_wanted' <- cloneWC inner_wanted
; return (implic { ic_wanted = inner_wanted' }) }
-- | Emits a new Wanted. Deals with both equalities and non-equalities.
emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
emitWanted origin pty
......@@ -188,7 +207,8 @@ emitWantedEq origin t_or_k role ty1 ty2
= do { hole <- newCoercionHole
; loc <- getCtLocM origin (Just t_or_k)
; emitSimple $ mkNonCanonical $
CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole, ctev_loc = loc }
CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
, ctev_nosh = WDeriv, ctev_loc = loc }
; return (mkHoleCo hole role ty1 ty2) }
where
pty = mkPrimEqPredRole role ty1 ty2
......@@ -201,6 +221,7 @@ emitWantedEvVar origin ty
; loc <- getCtLocM origin Nothing
; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
, ctev_pred = ty
, ctev_nosh = WDeriv
, ctev_loc = loc }
; emitSimple $ mkNonCanonical ctev
; return new_cv }
......
This diff is collapsed.
......@@ -287,16 +287,14 @@ EvVar for the coercion, fill the hole with the invented EvVar, and
then quantify over the EvVar. Not too tricky -- just some
impedence matching, really.
Note [Simplify *derived* constraints]
Note [Simplify cloned constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At this stage, we're simplifying constraints only for insolubility
and for unification. Note that all the evidence is quickly discarded.
We make this explicit by working over derived constraints, for which
there is no evidence. Using derived constraints also prevents solved
equalities from being written to coercion holes. If we don't do this,
We use a clone of the real constraint. If we don't do this,
then RHS coercion-hole constraints get filled in, only to get filled
in *again* when solving the implications emitted from tcRule. That's
terrible, so we avoid the problem by using derived constraints.
terrible, so we avoid the problem by cloning the constraints.
-}
......@@ -310,15 +308,16 @@ simplifyRule :: RuleName
simplifyRule name lhs_wanted rhs_wanted
= do { -- We allow ourselves to unify environment
-- variables: runTcS runs with topTcLevel
; tc_lvl <- getTcLevel
; lhs_clone <- cloneWC lhs_wanted
; rhs_clone <- cloneWC rhs_wanted
; insoluble <- runTcSDeriveds $
do { -- First solve the LHS and *then* solve the RHS
-- See Note [Solve order for RULES]
-- See Note [Simplify *derived* constraints]
lhs_resid <- solveWanteds $ toDerivedWC lhs_wanted
; rhs_resid <- solveWanteds $ toDerivedWC rhs_wanted
; return ( insolubleWC tc_lvl lhs_resid ||
insolubleWC tc_lvl rhs_resid ) }
-- See Note [Simplify cloned constraints]
lhs_resid <- solveWanteds lhs_clone
; rhs_resid <- solveWanteds rhs_clone
; return ( insolubleWC lhs_resid ||
insolubleWC rhs_resid ) }
; zonked_lhs_simples <- zonkSimples (wc_simple lhs_wanted)
......
This diff is collapsed.
This diff is collapsed.
......@@ -102,6 +102,7 @@ module TcType (
-- * Finding "exact" (non-dead) type variables
exactTyCoVarsOfType, exactTyCoVarsOfTypes,
splitDepVarsOfType, splitDepVarsOfTypes, TcDepVars(..), tcDepVarSet,
rewritableTyVarsOfTypes, rewritableTyVarsOfType,
-- * Extracting bound variables
allBoundVariables, allBoundVariabless,
......@@ -835,6 +836,23 @@ exactTyCoVarsOfType ty
exactTyCoVarsOfTypes :: [Type] -> TyVarSet
exactTyCoVarsOfTypes tys = mapUnionVarSet exactTyCoVarsOfType tys
rewritableTyVarsOfTypes :: [TcType] -> TcTyVarSet
rewritableTyVarsOfTypes tys = mapUnionVarSet rewritableTyVarsOfType tys
rewritableTyVarsOfType :: TcType -> TcTyVarSet
rewritableTyVarsOfType ty
= go ty
where
go (TyVarTy tv) = unitVarSet tv
go (LitTy {}) = emptyVarSet
go (TyConApp _ tys) = rewritableTyVarsOfTypes tys
go (AppTy fun arg) = go fun `unionVarSet` go arg
go (FunTy arg res) = go arg `unionVarSet` go res
go ty@(ForAllTy {}) = pprPanic "rewriteableTyVarOfType" (ppr ty)
go (CastTy ty _co) = go ty
go (CoercionTy _co) = emptyVarSet
{- *********************************************************************
* *
Bound variables in a type
......
......@@ -1509,8 +1509,10 @@ maybe_sym IsSwapped = mkSymCo
maybe_sym NotSwapped = id
swapOverTyVars :: TcTyVar -> TcTyVar -> Bool
-- See Note [Canonical orientation for tyvar/tyvar equality constraints]
swapOverTyVars tv1 tv2
| isFmvTyVar tv1 = False -- See Note [Fmv Orientation Invariant]
| isFmvTyVar tv2 = True
| Just lvl1 <- metaTyVarTcLevel_maybe tv1
-- If tv1 is touchable, swap only if tv2 is also
-- touchable and it's strictly better to update the latter
......@@ -1565,7 +1567,46 @@ canSolveByUnification tclvl tv xi
FlatSkol {} -> False
RuntimeUnk -> True
{-
{- Note [Fmv Orientation Invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* We always orient a constraint
fmv ~ alpha
with fmv on the left, even if alpha is
a touchable unification variable
Reason: doing it the other way round would unify alpha:=fmv, but that
really doesn't add any info to alpha. But a later constraint alpha ~
Int might unlock everything. Comment:9 of #12526 gives a detailed
example.
WARNING: I've gone to and fro on this one several times.
I'm now pretty sure that unifying alpha:=fmv is a bad idea!
So orienting with fmvs on the left is a good thing.
This example comes from IndTypesPerfMerge. (Others include
T10226, T10009.)
From the ambiguity check for
f :: (F a ~ a) => a
we get:
[G] F a ~ a
[WD] F alpha ~ alpha, alpha ~ a
From Givens we get
[G] F a ~ fsk, fsk ~ a
Now if we flatten we get
[WD] alpha ~ fmv, F alpha ~ fmv, alpha ~ a
Now, if we unified alpha := fmv, we'd get
[WD] F fmv ~ fmv, [WD] fmv ~ a
And now we are stuck.
So instead the Fmv Orientation Invariant puts te fmv on the
left, giving
[WD] fmv ~ alpha, [WD] F alpha ~ fmv, [WD] alpha ~ a
Now we get alpha:=a, and everything works out
Note [Prevent unification with type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We prevent unification with type families because of an uneasy compromise.
......
......@@ -42,6 +42,30 @@ showFromF fa = undefined
showFromF' :: (Show (FInv b), F (FInv b) ~ b) => b -> String
showFromF' = showFromF
{- [G] F (FInv b) ~ b
[W] FInv (F alpha) ~ alpha
[W] F alpha ~ b
-->
[G] g1: FInv b ~ fsk1
[G] g2: F fsk1 ~ fsk2
[G} g3: fsk2 ~ b
[W] F alpha ~ fmv1
[W] FInv fmv1 ~ fmv2
[W] fmv2 ~ alpha
[W] fmv1 ~ b
[D] d1: F alpha ~ fmv1
[D] d2: FInv fmv1 ~ fmv2
[D] d3: fmv2 ~ alpha
[D] d4: fmv1 ~ b
--> d2 + d4: [D] FInv b ~ fmv2
+ g1: [D] fmv2 ~ b
--> d3: b ~ alpha, and we are done
-}
{-------------------------------------------------------------------------------
In 7.10 the definition of showFromF' is not accepted, but it gets stranger.
In 7.10 we cannot _call_ showFromF at all, even at a concrete type. Below
......@@ -57,3 +81,36 @@ type instance FInv Int = Int
test :: String
test = showFromF (0 :: Int)
{-
[WD] FInv (F alpha) ~ alpha
[WD] F alpha ~ Int
-->
[WD] F alpha ~ fuv0
* [WD] FInv fuv0 ~ fuv1
[WD] fuv1 ~ alpha
[WD] fuv0 ~ Int
-->
[WD] F alpha ~ fuv0
[W] FInv fuv0 ~ fuv1
* [D] FInv Int ~ fuv1
[WD] fuv1 ~ alpha
[WD] fuv0 ~ Int
-->
[WD] F alpha ~ fuv0
[W] FInv fuv0 ~ fuv1
* [D] fuv1 ~ Int
[WD] fuv1 ~ alpha
[WD] fuv0 ~ Int
-->
[WD] F alpha ~ fuv0
[W] FInv fuv0 ~ fuv1
[D] alpha := Int
[WD] fuv1 ~ alpha
[WD] fuv0 ~ Int
-}
......@@ -21,3 +21,18 @@ instance Convert Int32 where
x :: Int8
x = down 8
{- From x = down 8
[WD] Num alpha
[WD] Convert alpha
[WD] Down alpha ~ Int8
--> superclasses
[D] Up (Down alpha) ~ alpha
--> substitute (Down alpha ~ Int8)
[D] Up Int8 ~ alpha
--> alpha := Int16
-}
{-# LANGUAGE TypeFamilies, MonoLocalBinds #-}
module T12526 where
type family P (s :: * -> *) :: * -> * -> *
type instance P Signal = Causal
type family S (p :: * -> * -> *) :: * -> *
type instance S Causal = Signal
class (P (S p) ~ p) => CP p
instance CP Causal
data Signal a = Signal
data Causal a b = Causal
shapeModOsci :: CP p => p Float Float
shapeModOsci = undefined
f :: Causal Float Float -> Bool
f = undefined
-- This fails
ping :: Bool
ping = let osci = shapeModOsci in f osci
-- This works
-- ping :: Bool
-- ping = f shapeModOsci
{-
osci :: p Float Float
[W] CP p, [D] P (S p) ~ p
-->
[W] CP p, [D] P fuv1 ~ fuv2, S p ~ fuv1, fuv2 ~ p
-->
p := fuv2
[W] CP fuv2, [D] P fuv1 ~ fuv2, S fuv2 ~ fuv1
-}
-- P (S p) ~ p
-- p Float Float ~ Causal Float Float
{-
P (S p) ~ p
p Float Float ~ Causal Float Float
--->
S p ~ fuv1 (FunEq)
P fuv1 ~ fuv2 (FunEq)
fuv2 ~ p
p F F ~ Causal F F
--->
p := fuv2
fuv2 ~ Causal
S fuv2 ~ fuv1 (FunEq)
P fuv1 ~ fuv2 (FunEq)
---> unflatten
fuv1 := S fuv2
fuv2 := Causal
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module T12538 where
data Tagged t a = Tagged a
type family Tag a where
Tag (Tagged t a) = Tagged t a
Tag a = Tagged Int a
class (r ~ Tag a) => TagImpl a r | a -> r where
tag :: a -> r
instance {-# OVERLAPPING #-} (r ~ Tag (Tagged t a)) => TagImpl (Tagged t a) r where
tag = id
#ifdef WRONG
instance {-# OVERLAPPING #-} (r ~ Tagged t a, r ~ Tag a) => TagImpl a r where
#else
instance {-# OVERLAPPING #-} (r ~ Tagged Int a, r ~ Tag a) => TagImpl a r where
#endif
tag = Tagged @Int
data family DF x
data instance DF (Tagged t a) = DF (Tagged t a)
class ToDF a b | a -> b where
df :: a -> b
instance (TagImpl a a', b ~ DF a') => ToDF a b where
df = DF . tag
main :: IO ()
main = pure ()
T12538.hs:37:8: error:
• Could not deduce: a' ~ Tagged Int a
from the context: (TagImpl a a', b ~ DF a')
bound by the instance declaration at T12538.hs:36:10-46
‘a'’ is a rigid type variable bound by
the instance declaration at T12538.hs:36:10-46
Expected type: a -> b
Actual type: a -> DF (Tagged Int a)
• In the expression: DF . tag
In an equation for ‘df’: df = DF . tag
In the instance declaration for ‘ToDF a b’
• Relevant bindings include df :: a -> b (bound at T12538.hs:37:3)
......@@ -4,7 +4,7 @@ TYPE SIGNATURES
emptyL :: forall a. ListColl a
insert :: forall c. Coll c => Elem c -> c -> c
test2 ::
forall a b c. (Elem c ~ (a, b), Coll c, Num a, Num b) => c -> c
forall a b c. (Elem c ~ (a, b), Num b, Num a, Coll c) => c -> c
TYPE CONSTRUCTORS
class Coll c where
type family Elem c :: * open
......
......@@ -17,7 +17,40 @@ instance Foo Char Int where
tickle = (+1)
test :: (Foo a b) => a -> a
test = back . tickle . there
test x = back (tickle (there x))
main :: IO ()
main = print $ test 'F'
{-
[G] Foo a b
[G] There a ~ b
[G] Back b ~ a
[W] Foo a beta -- from 'there'
[W] Foo alpha beta -- from tickle
[W] Foo a beta -- from back
[D] There a ~ beta
[D] Back beta ~ a
[D] There alpha ~ beta
[D] Back beta ~ alpha
-- Hence beta = b
-- alpha = a
[W] Foo a (There t_a1jL)
[W] Foo t_a1jL (There t_a1jL)
[W] Back (There t_a1jL) ~ t_a1jL
[D] There a ~ There t_a1jL
hence There t_a1jL ~ b
[D] Back (There t_a1jL) ~ a
[D] There t_a1jL ~ There t_a1jL
[D] Back (There t_a1jL) ~ t_a1jL
-}
......@@ -278,3 +278,5 @@ test('T12175', normal, compile, [''])
test('T12522', normal, compile, [''])
test('T12522b', normal, compile, [''])
test('T12676', normal, compile, [''])
test('T12526', normal, compile, [''])
test('T12538', normal, compile_fail, [''])
T2544.hs:17:12: error:
• Couldn't match type ‘IxMap r’ with ‘IxMap i1’
Expected type: IxMap (l :|: r) [Int]
Actual type: BiApp (IxMap l) (IxMap i1) [Int]
NB: ‘IxMap’ is a type function, and may not be injective
The type variable ‘i1’ is ambiguous
• In the expression: BiApp empty empty
In an equation for ‘empty’: empty = BiApp empty empty
In the instance declaration for ‘Ix (l :|: r)’
• Relevant bindings include
empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
T2544.hs:17:18: error:
• Couldn't match type ‘IxMap i0’ with ‘IxMap l’
Expected type: IxMap l [Int]
......@@ -10,15 +22,3 @@ T2544.hs:17:18: error:
In an equation for ‘empty’: empty = BiApp empty empty
• Relevant bindings include
empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
T2544.hs:17:24: error:
• Couldn't match type ‘IxMap i1’ with ‘IxMap r’
Expected type: IxMap r [Int]
Actual type: IxMap i1 [Int]
NB: ‘IxMap’ is a type function, and may not be injective
The type variable ‘i1’ is ambiguous
• In the second argument of ‘BiApp’, namely ‘empty’
In the expression: BiApp empty empty
In an equation for ‘empty’: empty = BiApp empty empty
• Relevant bindings include
empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)
T2627b.hs:20:24: error:
• Occurs check: cannot construct the infinite type:
t0 ~ Dual (Dual t0)
b0 ~ Dual (Dual b0)
arising from a use of ‘conn’
The type variable ‘t0’ is ambiguous
The type variable ‘b0’ is ambiguous
• In the expression: conn undefined undefined
In an equation for ‘conn’:
conn (Rd k) (Wr a r) = conn undefined undefined
......@@ -3,14 +3,14 @@ T3330c.hs:23:43: error:
• Couldn't match kind ‘* -> *’ with ‘*’
When matching types
f1 :: * -> *
Der f1 x :: *
Expected type: Der ((->) x) (Der f1 x)
f1 x :: *
Expected type: Der ((->) x) (f1 x)
Actual type: R f1
• In the first argument of ‘plug’, namely ‘rf’
In the first argument of ‘Inl’, namely ‘(plug rf df x)’
In the expression: Inl (plug rf df x)
• Relevant bindings include
x :: x (bound at T3330c.hs:23:29)
df :: Der f1 x (bound at T3330c.hs:23:25)
df :: f1 x (bound at T3330c.hs:23:25)
rf :: R f1 (bound at T3330c.hs:23:13)
plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:23:1)
T4179.hs:26:16: error:
• Couldn't match type ‘A3 (x (A2 (FCon x) -> A3 (FCon x)))’
with ‘A3 (FCon x)’
• Couldn't match type ‘A2 (x (A2 (FCon x) -> A3 (FCon x)))’
with ‘A2 (FCon x)’
Expected type: x (A2 (FCon x) -> A3 (FCon x))
-> A2 (FCon x) -> A3 (FCon x)
Actual type: x (A2 (FCon x) -> A3 (FCon x))
-> A2 (x (A2 (FCon x) -> A3 (FCon x)))
-> A3 (x (A2 (FCon x) -> A3 (FCon x)))
NB: ‘A3’ is a type function, and may not be injective
NB: ‘A2’ is a type function, and may not be injective
• In the first argument of ‘foldDoC’, namely ‘op’
In the expression: foldDoC op
In an equation for ‘fCon’: fCon = foldDoC op
......
T6123.hs:10:14: error:
• Occurs check: cannot construct the infinite type: t0 ~ Id t0
• Occurs check: cannot construct the infinite type: a0 ~ Id a0
arising from a use of ‘cid’
The type variable ‘t0’ is ambiguous
The type variable ‘a0’ is ambiguous
• In the expression: cid undefined
In an equation for ‘cundefined’: cundefined = cid undefined
• Relevant bindings include
cundefined :: t0 (bound at T6123.hs:10:1)
cundefined :: a0 (bound at T6123.hs:10:1)
......@@ -55,17 +55,17 @@ type family Intersect (l :: Inventory a) (r :: Inventory a) :: Inventory a where
Intersect l Empty = Empty
Intersect (More ls l) r = InterAppend (Intersect ls r) r l
type family InterAppend (l :: Inventory a)
(r :: Inventory a)
(one :: a)
type family InterAppend (l :: Inventory a)
(r :: Inventory a)
(one :: a)
:: Inventory a where
InterAppend acc Empty one = acc
InterAppend acc (More rs one) one = More acc one
InterAppend acc (More rs r) one = InterAppend acc rs one
type family BuriedUnder (sub :: Inventory [KeySegment])
(post :: [KeySegment])
(inv :: Inventory [KeySegment])
type family BuriedUnder (sub :: Inventory [KeySegment])
(post :: [KeySegment])
(inv :: Inventory [KeySegment])
:: Inventory [KeySegment] where
BuriedUnder Empty post inv = inv
BuriedUnder (More ps p) post inv = More ((ps `BuriedUnder` post) inv) (p `Under` post)
......@@ -82,9 +82,23 @@ foo :: Database inv
foo db k sub = buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db
-}
foogle :: Database inv
-> Sing post
-> Database sub
-> Maybe (Sing (Intersect (BuriedUnder sub post 'Empty) inv))
foogle db k sub = return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv))
addSub db k sub = do Nil :: Sing xxx <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
addSub db k sub = do Nil :: Sing xxx <- foogle db k sub
return $ Sub db k sub
{-
addSub :: Database inv -> Sing k -> Database sub -> Maybe (Database ((sub `BuriedUnder` k) inv))
addSub db k sub = do Nil :: Sing xxx <- foogle db sub k
-- Nil :: Sing ((sub `BuriedUnder` k) Empty `Intersect` inv) <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
-- Nil :: Sing Empty <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
-- Nil <- return (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
return $ Sub db k sub
-}