ghc-typelits-natnormalise 0.7.4 → 0.7.5
raw patch · 7 files changed
+342/−66 lines, 7 filesdep ~ghcPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependency ranges changed: ghc
API changes (from Hackage documentation)
- GHC.TypeLits.Normalise.Unify: subtractionToPred :: (Type, Type) -> (PredType, Kind)
+ GHC.TypeLits.Normalise.Unify: subtractionToPred :: TyCon -> (Type, Type) -> (PredType, Kind)
Files
- CHANGELOG.md +4/−0
- README.md +1/−1
- ghc-typelits-natnormalise.cabal +3/−3
- src/GHC/TypeLits/Normalise.hs +158/−48
- src/GHC/TypeLits/Normalise/Unify.hs +28/−5
- tests/ErrorTests.hs +129/−9
- tests/Tests.hs +19/−0
CHANGELOG.md view
@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.7.5 *June 17th 2021*+* Fixes [#52](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/50) Plugin doesn't solve inside arbitrary class constraints+* Build on GHC 9.2.0.20210422+ ## 0.7.4 *February 12th 2021* * Fixes [#50](https://github.com/clash-lang/ghc-typelits-natnormalise/issues/50) `x ^ C ~ y` erroneously deemed hard insoluable, a contradiction, when `C` is some type family other than +,-,*,^
README.md view
@@ -1,6 +1,6 @@ # ghc-typelits-natnormalise -[](http://travis-ci.org/clash-lang/ghc-typelits-natnormalise)+[](https://github.com/clash-lang/ghc-typelits-natnormalise/actions) [](https://hackage.haskell.org/package/ghc-typelits-natnormalise) [](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-natnormalise)
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise-version: 0.7.4+version: 0.7.5 synopsis: GHC typechecker plugin for types of kind GHC.TypeLits.Nat description: A type checker plugin for GHC that can solve /equalities/ and /inequalities/@@ -49,7 +49,7 @@ CHANGELOG.md cabal-version: >=1.10 tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,- GHC == 8.8.4, GHC == 8.10.3, GHC == 9.0.1+ GHC == 8.8.4, GHC == 8.10.4, GHC == 9.0.1 source-repository head type: git@@ -67,7 +67,7 @@ GHC.TypeLits.Normalise.Unify build-depends: base >=4.9 && <5, containers >=0.5.7.1 && <0.7,- ghc >=8.0.1 && <9.2,+ ghc >=8.0.1 && <9.4, ghc-tcplugins-extra >=0.3.1, transformers >=0.5.2.0 && < 0.6 if impl(ghc >= 9.0.0)
src/GHC/TypeLits/Normalise.hs view
@@ -169,6 +169,9 @@ import Data.Maybe (mapMaybe, catMaybes) import Data.Set (Set, empty, toList, notMember, fromList, union) import GHC.TcPluginM.Extra (tracePlugin, newGiven, newWanted)+#if MIN_VERSION_ghc(9,2,0)+import GHC.TcPluginM.Extra (lookupModule, lookupName)+#endif import qualified GHC.TcPluginM.Extra as TcPluginM #if MIN_VERSION_ghc(8,4,0) import GHC.TcPluginM.Extra (flattenGivens)@@ -178,27 +181,43 @@ -- GHC API #if MIN_VERSION_ghc(9,0,0) import GHC.Builtin.Names (knownNatClassName, eqTyConKey, heqTyConKey, hasKey)-import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon, typeNatKind)+import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon) import GHC.Builtin.Types.Literals- (typeNatAddTyCon, typeNatExpTyCon, typeNatLeqTyCon, typeNatMulTyCon,- typeNatSubTyCon)+ (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)+#if MIN_VERSION_ghc(9,2,0)+import GHC.Builtin.Types (naturalTy)+import GHC.Builtin.Types.Literals (typeNatCmpTyCon)+#else+import GHC.Builtin.Types (typeNatKind)+import GHC.Builtin.Types.Literals (typeNatLeqTyCon)+#endif import GHC.Core (Expr (..)) import GHC.Core.Coercion (CoercionHole, Role (..), mkUnivCo) import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred,- mkPrimEqPred, isEqPred, isEqPrimPred)+ mkPrimEqPred, isEqPred, isEqPrimPred, getClassPredTys_maybe) import GHC.Core.TyCo.Rep (Type (..), UnivCoProvenance (..))+import GHC.Core.TyCon (TyCon) import GHC.Core.Type (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe, typeKind) import GHC.Driver.Plugins (Plugin (..), defaultPlugin, purePlugin) import GHC.Tc.Plugin- (TcPluginM, newCoercionHole, tcLookupClass, tcPluginTrace, tcPluginIO)+ (TcPluginM, newCoercionHole, tcLookupClass, tcPluginTrace, tcPluginIO,+ newEvVar)+#if MIN_VERSION_ghc(9,2,0)+import GHC.Tc.Plugin (tcLookupTyCon)+#endif import GHC.Tc.Types (TcPlugin (..), TcPluginResult (..)) import GHC.Tc.Types.Constraint (Ct, CtEvidence (..), CtLoc, TcEvDest (..), ShadowInfo (WDeriv), ctEvidence, ctLoc, ctLocSpan, isGiven, isWanted, mkNonCanonical, setCtLoc, setCtLocSpan, isWantedCt, ctEvLoc, ctEvPred, ctEvExpr)-import GHC.Tc.Types.Evidence (EvTerm (..), evCast)+import GHC.Tc.Types.Evidence (EvTerm (..), evCast, evId)+#if MIN_VERSION_ghc(9,2,0)+import GHC.Data.FastString (fsLit)+import GHC.Types.Name.Occurrence (mkTcOcc)+import GHC.Unit.Module (mkModuleName)+#endif import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text) #else #if MIN_VERSION_ghc(8,5,0)@@ -213,20 +232,22 @@ import PrelNames (eqTyConKey, heqTyConKey) import TcEvidence (EvTerm (..)) #if MIN_VERSION_ghc(8,6,0)-import TcEvidence (evCast)+import TcEvidence (evCast, evId) #endif #if !MIN_VERSION_ghc(8,4,0) import TcPluginM (zonkCt) #endif import TcPluginM (TcPluginM, tcPluginTrace, tcPluginIO)-import Type (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe)+import Type+ (Kind, PredType, eqType, mkTyVarTy, tyConAppTyCon_maybe) import TysWiredIn (typeNatKind) import Coercion (CoercionHole, Role (..), mkUnivCo)-import TcPluginM (newCoercionHole, tcLookupClass)+import TcPluginM (newCoercionHole, tcLookupClass, newEvVar) import TcRnTypes (TcPlugin (..), TcPluginResult(..)) import TyCoRep (UnivCoProvenance (..)) import TcType (isEqPred)+import TyCon (TyCon) import TyCoRep (Type (..)) import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)@@ -241,7 +262,7 @@ isWantedCt) import Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, getEqPredTys, mkClassPred,- mkPrimEqPred)+ mkPrimEqPred, getClassPredTys_maybe) import Type (typeKind) #else import TcRnTypes@@ -250,9 +271,12 @@ isWantedCt) import TcType (typeKind) import Type- (EqRel (NomEq), PredTree (EqPred), classifyPredType, getEqPredTys, mkClassPred,- mkPrimEqPred)+ (EqRel (NomEq), PredTree (EqPred), classifyPredType, mkClassPred, mkPrimEqPred,+ getClassPredTys_maybe)+#if MIN_VERSION_ghc(8,4,0)+import Type (getEqPredTys) #endif+#endif #if MIN_VERSION_ghc(8,10,0) import Constraint (ctEvExpr)@@ -279,6 +303,11 @@ import GHC.TypeLits.Normalise.SOP import GHC.TypeLits.Normalise.Unify +#if MIN_VERSION_ghc(9,2,0)+typeNatKind :: Type+typeNatKind = naturalTy+#endif+ #if !MIN_VERSION_ghc(8,10,0) isEqPrimPred :: PredType -> Bool isEqPrimPred = isEqPred@@ -314,18 +343,39 @@ normalisePlugin :: Opts -> TcPlugin normalisePlugin opts = tracePlugin "ghc-typelits-natnormalise"- TcPlugin { tcPluginInit = tcPluginIO $ newIORef empty+ TcPlugin { tcPluginInit = lookupExtraDefs , tcPluginSolve = decideEqualSOP opts , tcPluginStop = const (return ()) } newtype OrigCt = OrigCt { runOrigCt :: Ct } +type ExtraDefs = (IORef (Set CType), TyCon)++lookupExtraDefs :: TcPluginM ExtraDefs+lookupExtraDefs = do+ ref <- tcPluginIO (newIORef empty)+#if !MIN_VERSION_ghc(9,2,0)+ return (ref, typeNatLeqTyCon)+#else+ md <- lookupModule myModule myPackage+ ordCond <- look md "OrdCond"+ return (ref, ordCond)+ where+ look md s = tcLookupTyCon =<< lookupName md (mkTcOcc s)+ myModule = mkModuleName "Data.Type.Ord"+ myPackage = fsLit "base"+#endif+ decideEqualSOP :: Opts- -> IORef (Set CType)- -- ^ Givens that is already generated.+ -> ExtraDefs+ -- ^ 1. Givens that is already generated. -- We have to generate new givens at most once; -- otherwise GHC will loop indefinitely.+ --+ --+ -- 2. For GHc 9.2: TyCon of Data.Type.Ord.OrdCond+ -- For older: TyCon of GHC.TypeLits.<=? -> [Ct] -> [Ct] -> [Ct]@@ -340,7 +390,7 @@ -- without this phase, we cannot derive, e.g., -- @IsVector UVector (Fin (n + 1))@ from -- @Unbox (1 + n)@!-decideEqualSOP opts gen'd givens _deriveds [] = do+decideEqualSOP opts (gen'd,ordCond) givens _deriveds [] = do done <- tcPluginIO $ readIORef gen'd #if MIN_VERSION_ghc(8,4,0) let simplGivens = flattenGivens givens@@ -349,7 +399,7 @@ #endif let reds = filter (\(_,(_,_,v)) -> null v || negNumbers opts) $- reduceGivens opts done simplGivens+ reduceGivens opts ordCond done simplGivens newlyDone = map (\(_,(prd, _,_)) -> CType prd) reds tcPluginIO $ modifyIORef' gen'd $ union (fromList newlyDone)@@ -360,7 +410,7 @@ -- Solving phase. -- Solves in/equalities on Nats and simplifiable constraints -- containing naturals.-decideEqualSOP opts gen'd givens _deriveds wanteds = do+decideEqualSOP opts (gen'd,ordCond) givens deriveds wanteds = do -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out #if MIN_VERSION_ghc(8,4,0) let simplGivens = givens ++ flattenGivens givens@@ -373,12 +423,16 @@ let wanteds0 = map (\ct -> (OrigCt ct, ct)) wanteds simplGivens <- mapM zonkCt givens #endif- let wanteds' = filter (isWanted . ctEvidence) wanteds- unit_wanteds = mapMaybe toNatEquality wanteds'+ let wanteds1 = filter (isWanted . ctEvidence) wanteds+ -- only return solve deriveds when there are wanteds to solve+ wanteds2 = case wanteds1 of+ [] -> []+ w -> w ++ deriveds+ unit_wanteds = mapMaybe (toNatEquality ordCond) wanteds2 nonEqs = filter (not . (\p -> isEqPred p || isEqPrimPred p) . ctEvPred . ctEvidence.snd) $ filter (isWanted. ctEvidence.snd) wanteds0 done <- tcPluginIO $ readIORef gen'd- let redGs = reduceGivens opts done simplGivens+ let redGs = reduceGivens opts ordCond done simplGivens newlyDone = map (\(_,(prd, _,_)) -> CType prd) redGs redGivens <- forM redGs $ \(origCt, (pred', evTerm, _)) -> mkNonCanonical' (ctLoc origCt) <$> newGiven (ctLoc origCt) pred' evTerm@@ -400,24 +454,28 @@ fmap (mkNonCanonical' (ctLoc ct)) . newWanted (ctLoc ct) tcPluginIO $ modifyIORef' gen'd $ union (fromList newlyDone)- let unit_givens = mapMaybe toNatEquality simplGivens- sr <- simplifyNats opts unit_givens unit_wanteds+ let unit_givens = mapMaybe (toNatEquality ordCond) simplGivens+ sr <- simplifyNats opts ordCond unit_givens unit_wanteds tcPluginTrace "normalised" (ppr sr)- reds <- forM reducible_wanteds $ \(origCt,(term, ws)) -> do- wants <- evSubtPreds origCt $ subToPred opts ws- return ((term, origCt), wants)+ reds <- forM reducible_wanteds $ \(origCt,(term, ws, wDicts)) -> do+ wants <- evSubtPreds origCt $ subToPred opts ordCond ws+ return ((term, origCt), wDicts ++ wants) case sr of Simplified evs -> do- let simpld = filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs- (solved',newWanteds) = second concat (unzip $ simpld ++ reds)+ let simpld = filter (not . isGiven . ctEvidence . (\((_,x),_) -> x)) evs+ -- Only solve derived when we solved a wanted+ simpld1 = case filter (isWanted . ctEvidence . (\((_,x),_) -> x)) evs ++ reds of+ [] -> []+ _ -> simpld+ (solved',newWanteds) = second concat (unzip $ simpld1 ++ reds) return (TcPluginOk solved' $ newWanteds ++ ineqForRedWants) Impossible eq -> return (TcPluginContradiction [fromNatEquality eq]) type NatEquality = (Ct,CoreSOP,CoreSOP) type NatInEquality = (Ct,(CoreSOP,CoreSOP,Bool)) -reduceGivens :: Opts -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]-reduceGivens opts done givens =+reduceGivens :: Opts -> TyCon -> Set CType -> [Ct] -> [(Ct, (Type, EvTerm, [PredType]))]+reduceGivens opts ordCond done givens = let nonEqs = [ ct | ct <- givens@@ -431,18 +489,18 @@ notMember (CType prd) done ) $ mapMaybe- (\ct -> (ct,) <$> tryReduceGiven opts givens ct)+ (\ct -> (ct,) <$> tryReduceGiven opts ordCond givens ct) nonEqs tryReduceGiven- :: Opts -> [Ct] -> Ct+ :: Opts -> TyCon -> [Ct] -> Ct -> Maybe (PredType, EvTerm, [PredType])-tryReduceGiven opts simplGivens ct = do+tryReduceGiven opts ordCond simplGivens ct = do let (mans, ws) = runWriter $ normaliseNatEverywhere $ ctEvPred $ ctEvidence ct ws' = [ p- | (p, _) <- subToPred opts ws+ | (p, _) <- subToPred opts ordCond ws , all (not . (`eqType` p). ctEvPred . ctEvidence) simplGivens ] pred' <- mans@@ -452,7 +510,7 @@ fromNatEquality (Left (ct, _, _)) = ct fromNatEquality (Right (ct, _)) = ct -reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)]))+reduceNatConstr :: [Ct] -> Ct -> TcPluginM (Maybe (EvTerm, [(Type, Type)], [Ct])) reduceNatConstr givens ct = do let pred0 = ctEvPred $ ctEvidence ct (mans, tests) = runWriter $ normaliseNatEverywhere pred0@@ -460,8 +518,35 @@ Nothing -> return Nothing Just pred' -> do case find ((`eqType` pred') .ctEvPred . ctEvidence) givens of- Nothing -> return Nothing- Just c -> return (Just (toReducedDict (ctEvidence c) pred0, tests))+ -- No existing evidence found+ Nothing -> case getClassPredTys_maybe pred' of+ -- Are we trying to solve a class instance?+ Just _ -> do+ -- Create new evidence binding for normalized class constraint+ evVar <- newEvVar pred'+ -- Bind the evidence to a new wanted normalized class constraint+ let wDict = mkNonCanonical+ (CtWanted pred' (EvVarDest evVar)+#if MIN_VERSION_ghc(8,2,0)+ WDeriv+#endif+ (ctLoc ct))+ -- Evidence for current wanted is simply the coerced binding for+ -- the new binding+ evCo = mkUnivCo (PluginProv "ghc-typelits-natnormalise")+ Representational+ pred' pred0+#if MIN_VERSION_ghc(8,6,0)+ ev = evId evVar `evCast` evCo+#else+ ev = EvId evVar `EvCast` evCo+#endif+ -- Use newly created coerced wanted as evidence, and emit the+ -- normalized wanted as a new constraint to solve.+ return (Just (ev, tests, [wDict]))+ _ -> return Nothing+ -- Use existing evidence+ Just c -> return (Just (toReducedDict (ctEvidence c) pred0, tests, [])) toReducedDict :: CtEvidence -> PredType -> EvTerm toReducedDict ct pred' =@@ -488,12 +573,15 @@ simplifyNats :: Opts -- ^ Allow negated numbers (potentially unsound!)+ -> TyCon+ -- ^ For GHc 9.2: TyCon of Data.Type.Ord.OrdCond+ -- For older: TyCon of GHC.TypeLits.<=? -> [(Either NatEquality NatInEquality,[(Type,Type)])] -- ^ Given constraints -> [(Either NatEquality NatInEquality,[(Type,Type)])] -- ^ Wanted constraints -> TcPluginM SimplifyResult-simplifyNats opts@Opts {..} eqsG eqsW = do+simplifyNats opts@Opts {..} ordCond eqsG eqsW = do let eqsG1 = map (second (const ([] :: [(Type,Type)]))) eqsG (varEqs,otherEqs) = partition isVarEqs eqsG1 fancyGivens = concatMap (makeGivensSet otherEqs) varEqs@@ -527,7 +615,7 @@ tcPluginTrace "unifyNats result" (ppr ur) case ur of Win -> do- evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred opts k)+ evs' <- maybe evs (:evs) <$> evMagic ct empty (subToPred opts ordCond k) simples subst evs' leqsG [] (xs ++ eqs') Lose -> if null evs && null eqs' then return (Impossible (fst eq))@@ -535,7 +623,7 @@ Draw [] -> simples subst evs [] (eq:xs) eqs' Draw subst' -> do evM <- evMagic ct empty (map unifyItemToPredType subst' ++- subToPred opts k)+ subToPred opts ordCond k) let leqsG' | isGiven (ctEvidence ct) = eqToLeq u' v' ++ leqsG | otherwise = leqsG case evM of@@ -557,7 +645,7 @@ tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u,u',ineqs)) case runWriterT (isNatural u') of Just (True,knW) -> do- evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred opts k)+ evs' <- maybe evs (:evs) <$> evMagic ct knW (subToPred opts ordCond k) simples subst evs' leqsG' xs eqs' Just (False,_) | null k -> return (Impossible (fst eq))@@ -577,7 +665,7 @@ smallest = solvedInEqSmallestConstraint solvedIneq case smallest of (True,kW) -> do- evs' <- maybe evs (:evs) <$> evMagic ct kW (subToPred opts k)+ evs' <- maybe evs (:evs) <$> evMagic ct kW (subToPred opts ordCond k) simples subst evs' leqsG' xs eqs' _ -> simples subst evs leqsG (eq:xs) eqs' @@ -632,14 +720,14 @@ -- If we allow negated numbers we simply do not emit the inequalities -- derived from the subtractions that are converted to additions with a -- negated operand-subToPred :: Opts -> [(Type, Type)] -> [(PredType, Kind)]-subToPred Opts{..}+subToPred :: Opts -> TyCon -> [(Type, Type)] -> [(PredType, Kind)]+subToPred Opts{..} ordCond | negNumbers = const []- | otherwise = map subtractionToPred+ | otherwise = map (subtractionToPred ordCond) -- Extract the Nat equality constraints-toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])-toNatEquality ct = case classifyPredType $ ctEvPred $ ctEvidence ct of+toNatEquality :: TyCon -> Ct -> Maybe (Either NatEquality NatInEquality,[(Type,Type)])+toNatEquality ordCond ct = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2 -> go t1 t2 _ -> Nothing@@ -656,7 +744,28 @@ , let (y',k2) = runWriter (normaliseNat y) -> Just (Left (ct, x', y'),k1 ++ k2) _ -> Nothing- | tc == typeNatLeqTyCon+#if MIN_VERSION_ghc(9,2,0)+ | tc == ordCond+ , [_,cmp,lt,eq,gt] <- xs+ , TyConApp tcCmpNat [x,y] <- cmp+ , tcCmpNat == typeNatCmpTyCon+ , TyConApp ltTc [] <- lt+ , ltTc == promotedTrueDataCon+ , TyConApp eqTc [] <- eq+ , eqTc == promotedTrueDataCon+ , TyConApp gtTc [] <- gt+ , gtTc == promotedFalseDataCon+ , let (x',k1) = runWriter (normaliseNat x)+ , let (y',k2) = runWriter (normaliseNat y)+ , let ks = k1 ++ k2+ = case tc' of+ _ | tc' == promotedTrueDataCon+ -> Just (Right (ct, (x', y', True)), ks)+ _ | tc' == promotedFalseDataCon+ -> Just (Right (ct, (x', y', False)), ks)+ _ -> Nothing+#else+ | tc == ordCond , [x,y] <- xs , let (x',k1) = runWriter (normaliseNat x) , let (y',k2) = runWriter (normaliseNat y)@@ -667,6 +776,7 @@ _ | tc' == promotedFalseDataCon -> Just (Right (ct, (x', y', False)), ks) _ -> Nothing+#endif go x y | isNatKind (typeKind x)
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -61,9 +61,16 @@ -- GHC API #if MIN_VERSION_ghc(9,0,0)-import GHC.Builtin.Types (boolTy, promotedTrueDataCon, typeNatKind)+import GHC.Builtin.Types (boolTy, promotedTrueDataCon) import GHC.Builtin.Types.Literals- (typeNatAddTyCon, typeNatExpTyCon, typeNatLeqTyCon, typeNatMulTyCon, typeNatSubTyCon)+ (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)+#if MIN_VERSION_ghc(9,2,0)+import GHC.Builtin.Types (naturalTy, promotedFalseDataCon)+import GHC.Builtin.Types.Literals (typeNatCmpTyCon)+#else+import GHC.Builtin.Types (typeNatKind)+import GHC.Builtin.Types.Literals (typeNatLeqTyCon)+#endif import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred) import GHC.Core.TyCon (TyCon) import GHC.Core.Type@@ -104,6 +111,11 @@ -- Used for haddock import GHC.TypeLits (Nat) +#if MIN_VERSION_ghc(9,2,0)+typeNatKind :: Type+typeNatKind = naturalTy+#endif+ newtype CType = CType { unCType :: Type } deriving Outputable @@ -304,12 +316,23 @@ = Nothing subtractionToPred- :: (Type,Type)+ :: TyCon+ -> (Type,Type) -> (PredType, Kind)-subtractionToPred (x,y) =- (mkPrimEqPred (mkTyConApp typeNatLeqTyCon [y,x])+subtractionToPred ordCond (x,y) =+#if MIN_VERSION_ghc(9,2,0)+ let cmpNat = mkTyConApp typeNatCmpTyCon [y,x]+ trueTc = mkTyConApp promotedTrueDataCon []+ falseTc = mkTyConApp promotedFalseDataCon []+ ordCmp = mkTyConApp ordCond+ [boolTy,cmpNat,trueTc,trueTc,falseTc]+ predTy = mkPrimEqPred ordCmp trueTc+ in (predTy,boolTy)+#else+ (mkPrimEqPred (mkTyConApp ordCond [y,x]) (mkTyConApp promotedTrueDataCon []) ,boolTy)+#endif -- | A substitution is essentially a list of (variable, 'SOP') pairs, -- but we keep the original 'Ct' that lead to the substitution being
tests/ErrorTests.hs view
@@ -112,7 +112,11 @@ testProxy6 = proxyFun6 (Proxy :: Proxy 7) testProxy6Errors =-#if __GLASGOW_HASKELL__ >= 900+#if __GLASGOW_HASKELL__ >= 902+ ["Expected: Proxy 7"+ ," Actual: Proxy (2 ^ k0)"+ ]+#elif __GLASGOW_HASKELL__ >= 900 ["Expected: Proxy (2 ^ k0)" ," Actual: Proxy 7" ]@@ -139,31 +143,69 @@ ] #endif -proxyInEq :: (a <= b) => Proxy a -> Proxy b -> ()+proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> () proxyInEq _ _ = () -proxyInEq' :: ((a <=? b) ~ 'False) => Proxy a -> Proxy b -> ()+proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> () proxyInEq' _ _ = () testProxy9 :: Proxy (a + 1) -> Proxy a -> () testProxy9 = proxyInEq testProxy9Errors =+#if __GLASGOW_HASKELL__ >= 902 [$(do localeEncoding <- runIO (getLocaleEncoding) if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"+ else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "(CmpNat (a + 1) a) 'True 'True 'False’"+ else litE $ stringL "(CmpNat (a + 1) a) 'True 'True 'False'"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "with ‘'True’"+ else litE $ stringL "with 'True"+ )+ ]+#else+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8 then litE $ stringL "Couldn't match type ‘(a + 1) <=? a’ with ‘'True’" else litE $ stringL "Couldn't match type `(a + 1) <=? a' with 'True" )]+#endif testProxy10 :: Proxy (a :: Nat) -> Proxy (a + 2) -> () testProxy10 = proxyInEq' testProxy10Errors =+#if __GLASGOW_HASKELL__ >= 902 [$(do localeEncoding <- runIO (getLocaleEncoding) if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"+ else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "(CmpNat a (a + 2)) 'True 'True 'False’"+ else litE $ stringL "(CmpNat a (a + 2)) 'True 'True 'False'"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "with ‘'False"+ else litE $ stringL "with 'False"+ )+ ]+#else+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8 then litE $ stringL "Couldn't match type ‘a <=? (a + 2)’ with ‘'False’" else litE $ stringL "Couldn't match type `a <=? (a + 2)' with 'False" )]+#endif testProxy11 :: Proxy (a :: Nat) -> Proxy a -> () testProxy11 = proxyInEq'@@ -179,31 +221,88 @@ testProxy12 = proxyInEq testProxy12Errors =+#if __GLASGOW_HASKELL__ >= 902 [$(do localeEncoding <- runIO (getLocaleEncoding) if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"+ else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "(CmpNat (a + b) (a + c)) 'True 'True 'False’"+ else litE $ stringL "(CmpNat (a + b) (a + c)) 'True 'True 'False'"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "with ‘'True’"+ else litE $ stringL "with 'True"+ )+ ]+#else+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8 then litE $ stringL "Couldn't match type ‘(a + b) <=? (a + c)’ with ‘'True’" else litE $ stringL "Couldn't match type `(a + b) <=? (a + c)' with 'True" )]+#endif testProxy13 :: Proxy (4*a) -> Proxy (2*a) ->() testProxy13 = proxyInEq testProxy13Errors =+#if __GLASGOW_HASKELL__ >= 902 [$(do localeEncoding <- runIO (getLocaleEncoding) if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"+ else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "(CmpNat (4 * a) (2 * a)) 'True 'True 'False’"+ else litE $ stringL "(CmpNat (4 * a) (2 * a)) 'True 'True 'False'"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "with ‘'True’"+ else litE $ stringL "with 'True"+ )+ ]+#else+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8 then litE $ stringL "Couldn't match type ‘(4 * a) <=? (2 * a)’ with ‘'True’" else litE $ stringL "Couldn't match type `(4 * a) <=? (2 * a)' with 'True" )]+#endif testProxy14 :: Proxy (2*a) -> Proxy (4*a) -> () testProxy14 = proxyInEq' testProxy14Errors =+#if __GLASGOW_HASKELL__ >= 902 [$(do localeEncoding <- runIO (getLocaleEncoding) if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"+ else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "(CmpNat (2 * a) (4 * a)) 'True 'True 'False’"+ else litE $ stringL "(CmpNat (2 * a) (4 * a)) 'True 'True 'False'"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "with ‘'False"+ else litE $ stringL "with 'False"+ )+ ]+#else+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8 then litE $ stringL "Couldn't match type ‘(2 * a) <=? (4 * a)’ with ‘'False’" else litE $ stringL "Couldn't match type `(2 * a) <=? (4 * a)' with 'False" )]+#endif type family CLog (b :: Nat) (x :: Nat) :: Nat type instance CLog 2 2 = 1@@ -232,11 +331,30 @@ x -> FS (test16 @(n-1) (x-1)) test16Errors =+#if __GLASGOW_HASKELL__ >= 902 [$(do localeEncoding <- runIO (getLocaleEncoding) if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "Couldn't match type ‘Data.Type.Ord.OrdCond"+ else litE $ stringL "Couldn't match type `Data.Type.Ord.OrdCond"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "(CmpNat 1 n) 'True 'True 'False’"+ else litE $ stringL "(CmpNat 1 n) 'True 'True 'False'"+ )+ ,$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8+ then litE $ stringL "with ‘'True’"+ else litE $ stringL "with 'True"+ )+ ]+#else+ [$(do localeEncoding <- runIO (getLocaleEncoding)+ if textEncodingName localeEncoding == textEncodingName utf8 then litE $ stringL "Couldn't match type ‘1 <=? n’ with ‘'True’" else litE $ stringL "Couldn't match type `1 <=? n' with 'True" )]+#endif data Dict c where Dict :: c => Dict c@@ -249,12 +367,7 @@ testProxy17 :: String testProxy17 = test17 (Proxy :: Proxy 17) Boo-test17Errors =- [$(do localeEncoding <- runIO (getLocaleEncoding)- if textEncodingName localeEncoding == textEncodingName utf8- then litE $ stringL "Couldn't match type ‘1 <=? n’ with ‘'True’"- else litE $ stringL "Couldn't match type `1 <=? n' with 'True"- )]+test17Errors = test16Errors test19f :: (1 <= n) => Proxy n -> Proxy n@@ -268,4 +381,11 @@ testProxy19 _ _ = test19f test19Errors =+#if __GLASGOW_HASKELL__ >= 902+ [ "Could not deduce: Data.Type.Ord.OrdCond"+ , "(CmpNat 1 (rp - m)) 'True 'True 'False"+ , "~ 'True"+ ]+#else ["Could not deduce: (1 <=? (rp - m)) ~ 'True"]+#endif
tests/Tests.hs view
@@ -4,10 +4,12 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -297,6 +299,23 @@ BT -> BT a' -> B0 a' predBNat (B0 x) = B1 (predBNat x)++-- issue 52 begin+type role Signal nominal representational+data Signal (dom :: Symbol) a = a :- Signal dom a++type role BitVector nominal+newtype BitVector (n :: Nat) = BV { unsafeToNatural :: Integer }++class Bundle (f :: Type -> Type) a res | f a -> res, f res -> a, a res -> f+bundle :: Bundle f a res => res -> f a+bundle = bundle++instance Bundle (Signal dom) (a,b) (Signal dom a, Signal dom b)++issue52 :: (1 <= n, KnownNat n) => (Signal dom (),Signal dom (BitVector (n-1+1))) -> Signal dom ((),BitVector n)+issue52 = bundle+-- issue 52 end proxyInEq1 :: Proxy a -> Proxy (a+1) -> () proxyInEq1 = proxyInEq