Skip to content

Commit

Permalink
Fixed mistake (ignored TVBinders in instance chains), cleaned up/fixe…
Browse files Browse the repository at this point in the history
…d existing tests
  • Loading branch information
gnumonik committed May 28, 2024
1 parent 89162e4 commit 5777b4e
Show file tree
Hide file tree
Showing 22 changed files with 148 additions and 46 deletions.
18 changes: 16 additions & 2 deletions src/Language/PureScript/CST/Convert.hs
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,10 @@ tvKind srcTok nm = do
$ "Error: Missing kind annotation for TyVar " <> Text.unpack nm
<> "\n at (or near): " <> prettyRange (srcTokenRange srcTok)
Just t -> pure t

prettyRange :: SourceRange -> String
prettyRange (SourceRange start end) = goPos start <> "-" <> goPos end
where
prettyRange (SourceRange start end) = goPos start <> "-" <> goPos end
goPos (SourcePos line col) = show line <> ":" <> show col

bindTv :: Text -> T.SourceType -> ConvertM ()
Expand Down Expand Up @@ -653,7 +655,19 @@ convertDeclaration fileName decl = case decl of
DeclInstanceChain _ insts -> do
let
chainId = mkChainId fileName $ startSourcePos $ instKeyword $ instHead $ sepHead insts
bindTypeVariables Nothing = pure ()
bindTypeVariables (Just (stok, bindings)) = traverse_ (goTvBind stok) (NE.toList bindings)
goTvBind stok = \case
TypeVarKinded (Wrapped _ (Labeled (_,nm) _ ki) _) -> do
let nm' = getIdent (nameValue nm)
ki' <- convertType fileName ki
bindTv nm' ki'
TypeVarName (_, nm) -> do
let nm' = Text.unpack . getIdent . nameValue $ nm
internalError $ "Error in instance declaration near " <> prettyRange (srcTokenRange stok)
<> "\n Missing kind annotation for Type Var '" <> nm' <> "'"
goInst ix inst@(Instance (InstanceHead _ _todo nameSep ctrs cls args) bd) = do
bindTypeVariables _todo
let ann' = uncurry (sourceAnnCommented fileName) $ instanceRange inst
clsAnn = findInstanceAnn cls args
cstrnt <- traverse (convertConstraint False fileName) $ maybe [] (toList . fst) ctrs
Expand All @@ -665,7 +679,7 @@ convertDeclaration fileName decl = case decl of
(qualified cls)
args'
(AST.ExplicitInstance instBinding)
traverse (uncurry goInst) $ zip [0..] (toList insts)
pure $ runConvert . uncurry goInst <$> zip [0..] (toList insts)
DeclDerive _ _ new (InstanceHead kw _todo nameSep ctrs cls args) -> do
let
chainId = mkChainId fileName $ startSourcePos kw
Expand Down
24 changes: 15 additions & 9 deletions src/Language/PureScript/TypeChecker/Types.hs
Original file line number Diff line number Diff line change
Expand Up @@ -375,30 +375,30 @@ instantiatePolyTypeWithUnknowns val printMe@(ForAll _ _ ident mbK ty _) = do
u <- freshTypeWithKind mbK
insertUnkName' u ident
result <- instantiatePolyTypeWithUnknowns val $ replaceTypeVars ident u ty
let msg = mkMsg result
goTraceM msg
--let msg = mkMsg result
--goTraceM msg
pure result
where
mkMsg (resultExpr,resultTy)
= "INSTANTIATE POLYTYPES WITH UNKNOWNS"
<> "\n EXPR: " <> renderValue 100 val
-- <> "\n EXPR: " <> renderValue 100 val
<> "\n TYPE: " <> prettyTypeStr printMe
<> "\n RESULT EXPR: " <> renderValue 100 resultExpr
<> "\n RESULT TYPE: " <> prettyTypeStr resultTy
-- <> "\n RESULT TYPE: " <> prettyTypeStr resultTy
<> spacer
instantiatePolyTypeWithUnknowns val printMe@(ConstrainedType _ con ty) = do
dicts <- getTypeClassDictionaries
hints <- getHints
result <- instantiatePolyTypeWithUnknowns (App val (TypeClassDictionary con dicts hints)) ty
goTraceM (mkMsg result)
-- goTraceM (mkMsg result)
pure result
where
mkMsg (resultExpr,resultTy)
= "INSTANTIATE POLYTYPES WITH UNKNOWNS"
<> "\n EXPR: " <> renderValue 100 val
-- <> "\n EXPR: " <> renderValue 100 val
<> "\n TYPE: " <> prettyTypeStr printMe
<> "\n RESULT EXPR: " <> renderValue 100 resultExpr
<> "\n RESULT TYPE: " <> prettyTypeStr resultTy
-- <> "\n RESULT TYPE: " <> prettyTypeStr resultTy
<> spacer
instantiatePolyTypeWithUnknowns val ty = return (val, ty)

Expand Down Expand Up @@ -704,8 +704,14 @@ inferBinder val (VarBinder ss name) = return $ M.singleton name (ss, val)
inferBinder val (ConstructorBinder ss ctor binders) = do
env <- getEnv
case M.lookup ctor (dataConstructors env) of
Just (_, _, ty, _) -> do
(_, fn) <- instantiatePolyTypeWithUnknowns (internalError "Data constructor types cannot contain constraints") ty
Just (_, tn, ty, _) -> do
let tn' = T.unpack $ runProperName tn
(_, fn) <- instantiatePolyTypeWithUnknowns
(internalError $ "Data constructor types cannot contain constraints: "
<> prettyTypeStr val
<> "\n while inferring binders for constructor of type: "
<> tn' <> "\n " <> prettyTypeStr ty
) ty
fn' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ fn
let (args, ret) = peelArgs fn'
expected = length args
Expand Down
2 changes: 1 addition & 1 deletion tests/purus/passing/4035/Other.purs
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,4 @@ module Other where


type Id :: Type -> Type
type Id (a :: Prim.Type) = a
type Id (a :: Type) = a
Binary file modified tests/purus/passing/4035/output/Other/externs.cbor
Binary file not shown.
2 changes: 1 addition & 1 deletion tests/purus/passing/4035/output/Other/index.cfn
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"builtWith":"0.0.1","comments":[],"dataTypes":{},"decls":[],"exports":[],"foreign":[],"imports":[{"annotation":{"meta":null,"sourceSpan":{"end":[5,29],"start":[1,1]}},"moduleName":["Builtin"]},{"annotation":{"meta":null,"sourceSpan":{"end":[5,29],"start":[1,1]}},"moduleName":["Prim"]}],"moduleName":["Other"],"modulePath":"tests/purus/passing/4035/Other.purs","reExports":{},"sourceSpan":{"end":[5,29],"start":[1,1]}}
{"builtWith":"0.0.1","comments":[],"dataTypes":{},"decls":[],"exports":[],"foreign":[],"imports":[{"annotation":{"meta":null,"sourceSpan":{"end":[5,24],"start":[1,1]}},"moduleName":["Builtin"]},{"annotation":{"meta":null,"sourceSpan":{"end":[5,24],"start":[1,1]}},"moduleName":["Prim"]}],"moduleName":["Other"],"modulePath":"tests/purus/passing/4035/Other.purs","reExports":{},"sourceSpan":{"end":[5,24],"start":[1,1]}}
2 changes: 1 addition & 1 deletion tests/purus/passing/4101/Lib.purs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module Lib where

-- newtype Const :: forall (j :: Type) (k :: j). Type -> k -> Type
newtype Const (a :: Prim.Type) (b :: Prim.Type) = Const a
newtype Const (a :: Type) (b :: Type) = Const a

data Unit = Unit

Expand Down
Binary file modified tests/purus/passing/4101/output/Lib/externs.cbor
Binary file not shown.
2 changes: 1 addition & 1 deletion tests/purus/passing/4101/output/Lib/index.cfn
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"builtWith":"0.0.1","comments":[],"dataTypes":{"Const":["newtype",[["a",{"annotation":[{"end":[4,30],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"}],["b",{"annotation":[{"end":[4,47],"name":"tests/purus/passing/4101/Lib.purs","start":[4,38]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"}]],[{"dataCtorAnn":[{"end":[4,58],"name":"tests/purus/passing/4101/Lib.purs","start":[4,49]},[]],"dataCtorFields":[[{"Ident":"value0"},{"annotation":[{"end":[4,58],"name":"tests/purus/passing/4101/Lib.purs","start":[4,57]},[]],"contents":{"kind":{"annotation":[{"end":[4,30],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"},"var":"a"},"tag":"TypeVar"}]],"dataCtorName":"Const"}]],"Unit":["data",[],[{"dataCtorAnn":[{"end":[6,17],"name":"tests/purus/passing/4101/Lib.purs","start":[6,11]},[]],"dataCtorFields":[],"dataCtorName":"Unit"}]]},"decls":[{"annotation":{"meta":null,"sourceSpan":{"end":[6,17],"start":[6,1]}},"bindType":"NonRec","expression":{"annotation":{"meta":null,"sourceSpan":{"end":[6,17],"start":[6,1]}},"constructorName":"Unit","fieldNames":[],"kind":"Constructor","type":{"annotation":[{"end":[0,0],"name":"","start":[0,0]},[]],"contents":[["Lib"],"Unit"],"tag":"TypeConstructor"},"typeName":"Unit"},"identifier":"Unit"},{"annotation":{"meta":null,"sourceSpan":{"end":[4,58],"start":[4,1]}},"bindType":"NonRec","expression":{"annotation":{"meta":{"metaType":"IsNewtype"},"sourceSpan":{"end":[4,58],"start":[4,1]}},"argument":"x","body":{"annotation":{"meta":null,"sourceSpan":{"end":[4,58],"start":[4,1]}},"kind":"Var","type":{"annotation":[{"end":[4,58],"name":"tests/purus/passing/4101/Lib.purs","start":[4,57]},[]],"contents":{"kind":{"annotation":[{"end":[4,30],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"},"var":"a"},"tag":"TypeVar"},"value":{"identifier":"x","sourcePos":[0,0]}},"kind":"Abs","type":{"annotation":[{"end":[0,0],"name":"","start":[0,0]},[]],"contents":{"identifier":"a","kind":{"annotation":[{"end":[4,30],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"},"skolem":null,"type":{"annotation":[{"end":[0,0],"name":"","start":[0,0]},[]],"contents":[{"annotation":[{"end":[0,0],"name":"","start":[0,0]},[]],"contents":[{"annotation":[{"end":[0,0],"name":"","start":[0,0]},[]],"contents":[["Prim"],"Function"],"tag":"TypeConstructor"},{"annotation":[{"end":[4,58],"name":"tests/purus/passing/4101/Lib.purs","start":[4,57]},[]],"contents":{"kind":{"annotation":[{"end":[4,30],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"},"var":"a"},"tag":"TypeVar"}],"tag":"TypeApp"},{"annotation":[{"end":[4,58],"name":"tests/purus/passing/4101/Lib.purs","start":[4,57]},[]],"contents":{"kind":{"annotation":[{"end":[4,30],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"},"var":"a"},"tag":"TypeVar"}],"tag":"TypeApp"},"visibility":"TypeVarInvisible"},"tag":"ForAll"}},"identifier":"Const"}],"exports":["Const","Unit"],"foreign":[],"imports":[{"annotation":{"meta":null,"sourceSpan":{"end":[9,23],"start":[1,1]}},"moduleName":["Builtin"]},{"annotation":{"meta":null,"sourceSpan":{"end":[9,23],"start":[1,1]}},"moduleName":["Prim"]}],"moduleName":["Lib"],"modulePath":"tests/purus/passing/4101/Lib.purs","reExports":{},"sourceSpan":{"end":[9,23],"start":[1,1]}}
{"builtWith":"0.0.1","comments":[],"dataTypes":{"Const":["newtype",[["a",{"annotation":[{"end":[4,25],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"}],["b",{"annotation":[{"end":[4,37],"name":"tests/purus/passing/4101/Lib.purs","start":[4,33]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"}]],[{"dataCtorAnn":[{"end":[4,48],"name":"tests/purus/passing/4101/Lib.purs","start":[4,39]},[]],"dataCtorFields":[[{"Ident":"value0"},{"annotation":[{"end":[4,48],"name":"tests/purus/passing/4101/Lib.purs","start":[4,47]},[]],"contents":{"kind":{"annotation":[{"end":[4,25],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"},"var":"a"},"tag":"TypeVar"}]],"dataCtorName":"Const"}]],"Unit":["data",[],[{"dataCtorAnn":[{"end":[6,17],"name":"tests/purus/passing/4101/Lib.purs","start":[6,11]},[]],"dataCtorFields":[],"dataCtorName":"Unit"}]]},"decls":[{"annotation":{"meta":null,"sourceSpan":{"end":[6,17],"start":[6,1]}},"bindType":"NonRec","expression":{"annotation":{"meta":null,"sourceSpan":{"end":[6,17],"start":[6,1]}},"constructorName":"Unit","fieldNames":[],"kind":"Constructor","type":{"annotation":[{"end":[0,0],"name":"","start":[0,0]},[]],"contents":[["Lib"],"Unit"],"tag":"TypeConstructor"},"typeName":"Unit"},"identifier":"Unit"},{"annotation":{"meta":null,"sourceSpan":{"end":[4,48],"start":[4,1]}},"bindType":"NonRec","expression":{"annotation":{"meta":{"metaType":"IsNewtype"},"sourceSpan":{"end":[4,48],"start":[4,1]}},"argument":"x","body":{"annotation":{"meta":null,"sourceSpan":{"end":[4,48],"start":[4,1]}},"kind":"Var","type":{"annotation":[{"end":[4,48],"name":"tests/purus/passing/4101/Lib.purs","start":[4,47]},[]],"contents":{"kind":{"annotation":[{"end":[4,25],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"},"var":"a"},"tag":"TypeVar"},"value":{"identifier":"x","sourcePos":[0,0]}},"kind":"Abs","type":{"annotation":[{"end":[0,0],"name":"","start":[0,0]},[]],"contents":{"identifier":"a","kind":{"annotation":[{"end":[4,25],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"},"skolem":null,"type":{"annotation":[{"end":[0,0],"name":"","start":[0,0]},[]],"contents":[{"annotation":[{"end":[0,0],"name":"","start":[0,0]},[]],"contents":[{"annotation":[{"end":[0,0],"name":"","start":[0,0]},[]],"contents":[["Prim"],"Function"],"tag":"TypeConstructor"},{"annotation":[{"end":[4,48],"name":"tests/purus/passing/4101/Lib.purs","start":[4,47]},[]],"contents":{"kind":{"annotation":[{"end":[4,25],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"},"var":"a"},"tag":"TypeVar"}],"tag":"TypeApp"},{"annotation":[{"end":[4,48],"name":"tests/purus/passing/4101/Lib.purs","start":[4,47]},[]],"contents":{"kind":{"annotation":[{"end":[4,25],"name":"tests/purus/passing/4101/Lib.purs","start":[4,21]},[]],"contents":[["Prim"],"Type"],"tag":"TypeConstructor"},"var":"a"},"tag":"TypeVar"}],"tag":"TypeApp"},"visibility":"TypeVarInvisible"},"tag":"ForAll"}},"identifier":"Const"}],"exports":["Const","Unit"],"foreign":[],"imports":[{"annotation":{"meta":null,"sourceSpan":{"end":[9,23],"start":[1,1]}},"moduleName":["Builtin"]},{"annotation":{"meta":null,"sourceSpan":{"end":[9,23],"start":[1,1]}},"moduleName":["Prim"]}],"moduleName":["Lib"],"modulePath":"tests/purus/passing/4101/Lib.purs","reExports":{},"sourceSpan":{"end":[9,23],"start":[1,1]}}
4 changes: 2 additions & 2 deletions tests/purus/passing/4105/Lib.purs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
module Lib where

type Template (col :: Prim.Type -> Prim.Type) = { bio :: col String }
type Identity (a :: Prim.Type) = a
type Template (col :: Type -> Type) = { bio :: col String }
type Identity (a :: Type) = a
type Patch = Template Identity
Binary file modified tests/purus/passing/4105/output/Lib/externs.cbor
Binary file not shown.
10 changes: 3 additions & 7 deletions tests/purus/passing/4310/Lib.purs
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
module Lib where

import Prim (Type, String, Int)

data Tuple (a :: Prim.Type) (b :: Prim.Type) = Tuple a b
data Tuple (a :: Type) (b :: Type) = Tuple a b

infixr 6 Tuple as /\
infixr 6 type Tuple as /\
Expand All @@ -12,13 +10,11 @@ mappend _ _ = "mappend"

infixr 5 mappend as <>

class Test (a :: Prim.Type) where
class Test (a :: Type) where
runTest :: a -> String

instance Test Int where
runTest _ = "4"

{- TODO/FIXME: Disabled while I figure out what to do here
instance (Test a, Test b) => Test (a /\ b) where
instance forall (a :: Type) (b :: Type). (Test a, Test b) => Test (a /\ b) where
runTest (a /\ b) = runTest a <> runTest b
-}
Binary file modified tests/purus/passing/4310/output/Lib/externs.cbor
Binary file not shown.
2 changes: 1 addition & 1 deletion tests/purus/passing/4310/output/Lib/index.cfn

Large diffs are not rendered by default.

34 changes: 32 additions & 2 deletions tests/purus/passing/4310/output/Lib/index.cfn.pretty
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@ Exports:
runTest,
Tuple,
mappend,
testInt
testInt,
test/\
Re-Exports:

Foreign:
Expand Down Expand Up @@ -39,4 +40,33 @@ runTest =
.runTest

mappend :: Prim.String -> Prim.String -> Prim.String
mappend = \(v: Prim.String) -> \(v1: Prim.String) -> ("mappend": Prim.String)
mappend = \(v: Prim.String) -> \(v1: Prim.String) -> ("mappend": Prim.String)

test/\ :: forall (a :: Prim.Type) (b :: Prim.Type). Lib.Test$Dict (a :: Prim.Type) -> Lib.Test$Dict (b :: Prim.Type) -> Lib.Test$Dict (Lib.Tuple (a :: Prim.Type) (b :: Prim.Type))
test/\ =
\(dictTest: Lib.Test$Dict (a :: Prim.Type)) ->
\(dictTest1: Lib.Test$Dict (b :: Prim.Type)) ->
(Test$Dict: {
runTest :: (Lib.Tuple (a :: Prim.Type) (b :: Prim.Type)) ->
Prim.String
} ->
Lib.Test$Dict (Lib.Tuple (a :: Prim.Type) (b :: Prim.Type)))
({
runTest: \(v: (Lib.Tuple (a :: Prim.Type) (b :: Prim.Type))) ->
case (v: (Lib.Tuple (a :: Prim.Type) (b :: Prim.Type))) of
Tuple a b ->
(mappend: Prim.String -> Prim.String -> Prim.String)
((runTest: forall (@a :: Prim.Type). Lib.Test$Dict
(a :: Prim.Type) ->
(a :: Prim.Type) -> Prim.String)
(dictTest: Lib.Test$Dict (a :: Prim.Type))
(a: (a :: Prim.Type)))
((runTest: forall (@a :: Prim.Type). Lib.Test$Dict
(a :: Prim.Type) ->
(a :: Prim.Type) -> Prim.String)
(dictTest1: Lib.Test$Dict (b :: Prim.Type))
(b: (b :: Prim.Type)))
}: {
runTest :: (Lib.Tuple (a :: Prim.Type) (b :: Prim.Type)) ->
Prim.String
})
16 changes: 5 additions & 11 deletions tests/purus/passing/ForeignKind/Lib.purs
Original file line number Diff line number Diff line change
Expand Up @@ -48,18 +48,12 @@ proxy3 = NatProxy
-- TODO: Don't require annotations in fundep
class AddNat (l :: Nat) (r :: Nat) (o :: Nat) | l -> r o

{-
instance addNatZero
:: AddNat Zero (r :: Nat) (r :: Nat)
instance forall (r :: Nat). AddNat Zero r r


-- TODO: Bind kinds
instance addNatSucc
:: AddNat ((l) :: Nat) ((r) :: Nat) ((o) :: Nat)
=> AddNat (Succ ((l) :: Nat)) ((r) :: Nat) (Succ ((o) :: Nat))
instance forall (l :: Nat) (r :: Nat) (o :: Nat). AddNat l r o
=> AddNat (Succ l) r (Succ o)

-- use of class
--addNat :: forall (l :: Nat) (r :: Nat) (o :: Nat). AddNat l r o => NatProxy l -> NatProxy r -> NatProxy o
--addNat _ _ = NatProxy
-}
addNat :: forall (l :: Nat) (r :: Nat) (o :: Nat). AddNat l r o => NatProxy l -> NatProxy r -> NatProxy o
addNat _ _ = NatProxy
Binary file not shown.
Loading

0 comments on commit 5777b4e

Please sign in to comment.