ghc-typelits-knownnat 0.2 → 0.2.1
raw patch · 6 files changed
+48/−33 lines, 6 files
Files
- CHANGELOG.md +4/−0
- README.md +3/−1
- ghc-typelits-knownnat.cabal +1/−2
- src/GHC/TypeLits/KnownNat.hs +9/−6
- src/GHC/TypeLits/KnownNat/Solver.hs +22/−12
- tests/TestFunctions.hs +9/−12
CHANGELOG.md view
@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.2.1 *August 19th 2016*+* Fixes bugs:+ * Source location of derived wanted constraints is, erroneously, always set to line 1, column 1+ ## 0.2 *August 17th 2016* * New features: * Handle `GHC.TypeLits.-`
README.md view
@@ -52,13 +52,15 @@ type family Max (a :: Nat) (b :: Nat) :: Nat where Max 0 b = b Max a b = If (a <=? b) b a++$(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol ``` and corresponding `KnownNat2` instance: ```haskell instance (KnownNat a, KnownNat b) => KnownNat2 "TestFunctions.Max" a b where- type KnownNatF2 "TestFunctions.Max" = MaxSym2+ type KnownNatF2 "TestFunctions.Max" = MaxSym0 natSing2 = let x = natVal (Proxy @ a) y = natVal (Proxy @ b) z = max x y
ghc-typelits-knownnat.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-knownnat-version: 0.2+version: 0.2.1 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -118,7 +118,6 @@ TypeApplications TypeFamilies TypeFamilyDependencies- TypeInType TypeOperators UndecidableInstances if flag(deverror)
src/GHC/TypeLits/KnownNat.hs view
@@ -24,16 +24,19 @@ of @Max@, then you must define: @-\{\-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables,- TypeApplications, TypeFamilies, TypeInType, TypeOperators,- UndecidableInstances, TemplateHaskell \#-\}+\{\-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,+ MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,+ TypeApplications, TypeFamilies, TypeOperators,+ UndecidableInstances \#-\} -import Data.Proxy (Proxy (..))-import Data.Singletons (Apply, type (~>))+import Data.Proxy (Proxy (..))+import Data.Singletons.TH (genDefunSymbols) import GHC.TypeLits.KnownNat +$(genDefunSymbols [''Max]) -- creates the \'MaxSym0\' symbol+ instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where- type 'KnownNatF2' $('nameToSymbol' ''Max) = MaxSym2+ type 'KnownNatF2' $('nameToSymbol' ''Max) = MaxSym0 natSing2 = let x = natVal (Proxy @a) y = natVal (Proxy @b) z = max x y
src/GHC/TypeLits/KnownNat/Solver.hs view
@@ -51,13 +51,15 @@ type family Max (a :: Nat) (b :: Nat) :: Nat where Max 0 b = b Max a b = If (a <=? b) b a++$(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol @ and corresponding @KnownNat2@ instance: @ instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where- type KnownNatF2 \"TestFunctions.Max\" = MaxSym2+ type KnownNatF2 \"TestFunctions.Max\" = MaxSym0 natSing2 = let x = natVal (Proxy @ a) y = natVal (Proxy @ b) z = max x y@@ -115,8 +117,9 @@ import PrelNames (knownNatClassName) import TcEvidence (EvTerm (..), mkEvCast, mkTcSymCo, mkTcTransCo) import TcPluginM (TcPluginM, tcLookupClass, getInstEnvs, zonkCt)-import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvPred,- ctEvTerm, ctLoc, isWanted, mkNonCanonical)+import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvLoc,+ ctEvPred, ctEvTerm, ctLoc, ctLocSpan, isWanted,+ mkNonCanonical, setCtLoc, setCtLocSpan) import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon) import Type (PredTree (ClassPred), PredType, classifyPredType, dropForAlls, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, piResultTys,@@ -183,13 +186,15 @@ type family Max (a :: Nat) (b :: Nat) :: Nat where Max 0 b = b Max a b = If (a <=? b) b a++$(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol @ and corresponding @KnownNat2@ instance: @ instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where- type KnownNatF2 \"TestFunctions.Max\" = MaxSym2+ type KnownNatF2 \"TestFunctions.Max\" = MaxSym0 natSing2 = let x = natVal (Proxy @ a) y = natVal (Proxy @ b) z = max x y@@ -330,9 +335,16 @@ go_arg ty = case lookup (CType ty) givens of Just ev -> return (ev,[]) _ -> do- wanted <- newWanted (ctLoc ct) ty- let ev = ctEvTerm wanted- return (ev,[mkNonCanonical wanted])+ -- Create a new wanted constraint+ wantedCtEv <- newWanted (ctLoc ct) ty+ let ev = ctEvTerm wantedCtEv+ wanted = mkNonCanonical wantedCtEv+ -- Set the source-location of the new wanted constraint to the source+ -- location of the [W]anted constraint we are currently trying to solve+ let ct_ls = ctLocSpan (ctLoc ct)+ ctl = ctEvLoc wantedCtEv+ wanted' = setCtLoc wanted (setCtLocSpan ctl ct_ls)+ return (ev,[wanted']) -- Fall through case: look up the normalised [W]anted constraint in the list -- of [G]iven constraints.@@ -362,11 +374,9 @@ exploded = map (normaliseNat . subWant &&& id) knowns -- interesting cases for us are those where -- wanted and given only differ by a constant- examine (diff,entire) =- case diff of- S [P [I n]] -> Just (entire, n)- _ -> Nothing- interesting = mapMaybe examine exploded+ examineDiff (S [P [I n]]) entire = Just (entire,n)+ examineDiff _ _ = Nothing+ interesting = mapMaybe (uncurry examineDiff) exploded -- convert the first suitable evidence ((h,corr):_) <- pure interesting let x = case corr of
tests/TestFunctions.hs view
@@ -1,12 +1,13 @@-{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables,- TypeApplications, TypeFamilies, TypeInType, TypeOperators,- UndecidableInstances, TemplateHaskell #-}+{-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures,+ MultiParamTypeClasses, ScopedTypeVariables, TemplateHaskell,+ TypeApplications, TypeFamilies, TypeOperators,+ UndecidableInstances #-} module TestFunctions where -import Data.Proxy (Proxy (..))-import Data.Singletons (Apply, type (~>))-import Data.Type.Bool (If)+import Data.Proxy (Proxy (..))+import Data.Singletons.TH (genDefunSymbols)+import Data.Type.Bool (If) import GHC.TypeLits.KnownNat import GHC.TypeLits @@ -14,14 +15,10 @@ Max 0 b = b -- See [Note: single equation TFs are treated like synonyms] Max a b = If (a <=? b) b a -data MaxSym1 :: Nat -> Nat ~> Nat-data MaxSym2 :: Nat ~> Nat ~> Nat--type instance Apply MaxSym2 a = (MaxSym1 a)-type instance Apply (MaxSym1 a) b = Max a b+genDefunSymbols [''Max] instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where- type KnownNatF2 $(nameToSymbol ''Max) = MaxSym2+ type KnownNatF2 $(nameToSymbol ''Max) = MaxSym0 natSing2 = let x = natVal (Proxy @ a) y = natVal (Proxy @ b) z = max x y