Solve unsolved class constraints during whnf

This requires some changes to the normalisation machinery and to the
elaborator.

* The whnf function is now parameterised by how it should handle
unsolved class constraints. When typechecking, this parameter is the
class instance elaborator.
* The class instance elaborator is now parameterised by what it should
do with constraints it still didn't manage to solve. When normalising,
we want to keep the constraints as the `UnsolvedConstraint` global,
since it allows the type of the constraint to contain bound variables.
When generalising, we want to (like before) make the constraints `Exist`
metavars, such that they are picked up as free vars that can be
generalised.

Fixes #48.

The elaboration during normalisation will not take into account local
constraints (e.g. stemming from `MyClass a =>` constraints in a type
signature), but I believe this is not necessary since those constraints
are still unknown and will not reduce further anyway. So I think it's OK
to leave those for the full elaboration pass. (I might be wrong
though...)

src/Backend/SLam.hs

@@ -16,7 +16,7 @@ import qualified Syntax.Sized.SLambda as SLambda
 import VIX
 
 slamSized :: AbstractM -> VIX LambdaM
-slamSized e = SLambda.Anno <$> slam e <*> (slam =<< whnf' True =<< typeOf e)
+slamSized e = SLambda.Anno <$> slam e <*> (slam =<< whnfExpandingTypeReps =<< typeOf e)
 
 slam :: AbstractM -> VIX LambdaM
 slam expr = do
@@ -33,10 +33,10 @@ slam expr = do
     Abstract.Global g -> return $ SLambda.Global g
     Abstract.Lit l -> return $ SLambda.Lit l
     Abstract.Pi {} -> do
-      t <- whnf' True $ Abstract.Global Builtin.PiTypeName
+      t <- whnfExpandingTypeReps $ Abstract.Global Builtin.PiTypeName
       slam t
     Abstract.Lam h p t s -> do
-      t' <- whnf' True t
+      t' <- whnfExpandingTypeReps t
       v <- forall h p t'
       e <- slamSized $ instantiate1 (pure v) s
       rep <- slam t'
@@ -74,7 +74,7 @@ slam expr = do
       let scope' = abstract abstr body
       return $ SLambda.Let ds' scope'
     Abstract.ExternCode c retType -> do
-        retType' <- slam =<< whnf' True retType
+        retType' <- slam =<< whnfExpandingTypeReps retType
         c' <- slamExtern c
         return $ SLambda.Anno (SLambda.ExternCode c') retType'
   modifyIndent pred
@@ -93,7 +93,7 @@ slamBranches (ConBranches cbrs) = do
       let vs = fst <$> tele'
           abstr = teleAbstraction vs
           t = instantiateTele pure vs s
-      trep <- slam =<< whnf' True t
+      trep <- slam =<< whnfExpandingTypeReps t
       v <- forall h p t
       return (v, TeleArg h p $ abstract abstr trep)
     let vs = fst <$> tele'
@@ -118,7 +118,7 @@ slamExtern (Extern lang parts)
   = fmap (Extern lang) $ forM parts $ \part -> case part of
     ExternPart str -> return $ ExternPart str
     ExprMacroPart e -> ExprMacroPart <$> slamSized e
-    TypeMacroPart t -> TypeMacroPart <$> (slam =<< whnf' True t)
+    TypeMacroPart t -> TypeMacroPart <$> (slam =<< whnfExpandingTypeReps t)
     TargetMacroPart m -> return $ TargetMacroPart m
 
 slamDef

src/Builtin/Names.hs

@@ -15,6 +15,8 @@ pattern BuiltinModuleName <- ((==) "Sixten.Builtin" -> True) where BuiltinModule
 
 pattern UnsolvedConstraintName :: QName
 pattern UnsolvedConstraintName <- ((==) "Sixten.Builtin.UnsolvedConstraint" -> True) where UnsolvedConstraintName = "Sixten.Builtin.UnsolvedConstraint"
+pattern UnsolvedConstraint :: Expr v -> Expr v
+pattern UnsolvedConstraint typ = App (Global UnsolvedConstraintName) Explicit typ
 
 pattern IntName :: QName
 pattern IntName <- ((==) "Sixten.Builtin.Int" -> True) where IntName = "Sixten.Builtin.Int"

src/Frontend/Declassify.hs

@@ -158,7 +158,7 @@ deinstance qname@(QName modName name) loc (PatInstanceDef methods) typ = located
           , loc
           , TopLevelPatDefinition
             $ PatDefinition
-              Abstract
+              Concrete
               IsInstance
               $ pure
               $ Clause mempty

src/Inference/Class.hs

@@ -16,7 +16,9 @@ import Data.Vector(Vector)
 import qualified Data.Vector as Vector
 import Data.Void
 
+import qualified Builtin.Names as Builtin
 import Inference.Monad
+import qualified Inference.Normalise as Normalise
 import Inference.Subtype
 import Meta
 import Syntax
@@ -46,39 +48,35 @@ withVars
 withVars xs b = foldr withVar b xs
 
 elabUnsolvedConstraint
-  :: Exists Plicitness Expr
-  -> MetaA
-  -> Infer AbstractM
-elabUnsolvedConstraint ref var = do
-  let typ = metaType var
-  case typ of
-    (appsView -> (Global className, _)) -> do
-      -- Replace existentials in typ with universals
-      (uniType, uniVarMap) <- universalise typ
-      -- Try subsumption on all instances of the class until a match is found
-      globalClassInstances <- gets $ HashMap.lookupDefault mempty className . vixClassInstances
-      -- TODO universalise localInstances
-      localInstances <- asks constraints
-      let candidates = [(Global g, vacuous t) | (g, t) <- globalClassInstances]
-            <> localInstances
-      matchingInstances <- forM candidates $ \(inst, instType) -> tryMaybe $ do
-        f <- subtype instType uniType
-        f inst
-      case catMaybes matchingInstances of
-        [] -> do
-          let result = pure var
-          logMeta 25 "No matching instance" result
-          return result
-        matchingInstance:_ -> do
-          -- Elaborate any constraints introduced by the matching instance
-          elabInstance <- elabExpr matchingInstance
-          -- Replace the universals from before with the original existentials
-          result <- deuniversalise uniVarMap elabInstance
-          solve ref result
-          logMeta 25 "Matching instance" result
-          logMeta 25 "Matching instance typ" typ
-          return result
-    _ -> throwLocated "Malformed constraint" -- TODO error message
+  :: (AbstractM -> Infer AbstractM)
+  -> AbstractM
+  -> Infer (Maybe AbstractM)
+elabUnsolvedConstraint mkConstraint typ = case typ of
+  (appsView -> (Global className, _)) -> do
+    -- Replace existentials in typ with universals
+    (uniType, uniVarMap) <- universalise typ
+    -- Try subsumption on all instances of the class until a match is found
+    globalClassInstances <- gets $ HashMap.lookupDefault mempty className . vixClassInstances
+    -- TODO universalise localInstances
+    localInstances <- asks constraints
+    let candidates = [(Global g, vacuous t) | (g, t) <- globalClassInstances]
+          <> localInstances
+    matchingInstances <- forM candidates $ \(inst, instType) -> tryMaybe $ do
+      f <- subtype instType uniType
+      f inst
+    case catMaybes matchingInstances of
+      [] -> do
+        logVerbose 25 "No matching instance"
+        return Nothing
+      matchingInstance:_ -> do
+        -- Elaborate any constraints introduced by the matching instance
+        elabInstance <- elabExpr mkConstraint matchingInstance
+        -- Replace the universals from before with the original existentials
+        result <- deuniversalise uniVarMap elabInstance
+        logMeta 25 "Matching instance" result
+        logMeta 25 "Matching instance typ" typ
+        return $ Just result
+  _ -> throwLocated "Malformed constraint" -- TODO error message
 
 -- | Replace existentials in typ with universals and return the mapping from
 -- the new variables to the old existentials.
@@ -102,96 +100,109 @@ deuniversalise rtl = bindM go
     go v = return $ pure $ fromMaybe v $ HashMap.lookup v rtl
 
 elabVar
-  :: MetaA
+  :: (AbstractM -> Infer AbstractM)
+  -> MetaA
   -> Infer AbstractM
-elabVar var@MetaVar { metaRef = Exists ref } = do
+elabVar mkConstraint var@MetaVar { metaRef = Exists ref } = do
   sol <- solution ref
   case (sol, metaData var) of
-    (Left _, Constraint) -> elabUnsolvedConstraint ref var
+    (Left _, Constraint) -> do
+      mresult <- elabUnsolvedConstraint mkConstraint $ metaType var
+      case mresult of
+        Nothing -> mkConstraint $ metaType var
+        Just result -> do
+          solve ref result
+          return result
     (Left _, Implicit) -> return $ pure var
     (Left _, Explicit) -> return $ pure var
-    (Right expr, _) -> elabExpr expr
-elabVar var@MetaVar { metaRef = Forall } = return $ pure var
-elabVar var@MetaVar { metaRef = LetRef {} } = return $ pure var
+    (Right expr, _) -> elabExpr mkConstraint expr
+elabVar _ var@MetaVar { metaRef = Forall } = return $ pure var
+elabVar _ var@MetaVar { metaRef = LetRef {} } = return $ pure var
 
 elabExpr
-  :: AbstractM
+  :: (AbstractM -> Infer AbstractM)
+  -> AbstractM
   -> Infer AbstractM
-elabExpr expr = do
+elabExpr mkConstraint expr = do
   logMeta 40 "elabExpr expr" expr
   modifyIndent succ
   result <- case expr of
-    UnsolvedConstraint typ -> do
-      v <- exists mempty Constraint typ -- TODO maybe we don't need the var here?
-      elabVar v
-    Var v -> elabVar v
+    Builtin.UnsolvedConstraint typ -> do
+      mresult <- elabUnsolvedConstraint mkConstraint typ
+      case mresult of
+        Nothing -> mkConstraint typ
+        Just result -> return result
+    Var v -> elabVar mkConstraint v
     Global g -> return $ Global g
     Con c -> return $ Con c
     Lit l -> return $ Lit l
     Pi h p t s -> absCase Pi h p t s
     Lam h p t s -> absCase Lam h p t s
-    App e1 p e2 -> App <$> elabExpr e1 <*> pure p <*> elabExpr e2
-    Let ds scope -> elabLet ds scope
-    Case e brs t -> Case <$> elabExpr e <*> elabBranches brs <*> elabExpr t
-    ExternCode ext t -> ExternCode <$> mapM elabExpr ext <*> elabExpr t
+    App e1 p e2 -> App <$> go e1 <*> pure p <*> go e2
+    Let ds scope -> elabLet mkConstraint ds scope
+    Case e brs t -> Case <$> go e <*> elabBranches mkConstraint brs <*> go t
+    ExternCode ext t -> ExternCode <$> mapM go ext <*> go t
   modifyIndent pred
   logMeta 40 "elabExpr result" result
   return result
   where
+    go = elabExpr mkConstraint
     absCase c h p t s = do
-      t' <- elabExpr t
+      t' <- go t
       v <- forall h p t'
       let e = instantiate1 (pure v) s
-      e' <- enterLevel $ withVar v $ elabExpr e
+      e' <- enterLevel $ withVar v $ go e
       s' <- abstract1M v e'
       return $ c h p t' s'
 
 elabLet
-  :: LetRec Expr MetaA
+  :: (AbstractM -> Infer AbstractM)
+  -> LetRec Expr MetaA
   -> Scope LetVar Expr MetaA
   -> Infer (Expr MetaA)
-elabLet ds scope = do
+elabLet mkConstraint ds scope = do
   vs <- forMLet ds $ \h _ t -> do
-    t' <- elabExpr t
+    t' <- elabExpr mkConstraint t
     forall h Explicit t'
   let abstr = letAbstraction vs
   ds' <- iforMLet ds $ \i h s _ -> do
     let e = instantiateLet pure vs s
-    e' <- elabExpr e
+    e' <- elabExpr mkConstraint e
     s' <- abstractM abstr e'
     return $ LetBinding h s' $ metaType $ vs Vector.! i
   let expr = instantiateLet pure vs scope
-  expr' <- elabExpr expr
+  expr' <- elabExpr mkConstraint expr
   scope' <- abstractM abstr expr'
   return $ Let (LetRec ds') scope'
 
 elabBranches
-  :: Branches QConstr Plicitness Expr MetaA
+  :: (AbstractM -> Infer AbstractM)
+  -> Branches QConstr Plicitness Expr MetaA
   -> Infer (Branches QConstr Plicitness Expr MetaA)
-elabBranches (ConBranches cbrs) = do
+elabBranches mkConstraint (ConBranches cbrs) = do
   cbrs' <- forM cbrs $ \(ConBranch qc tele brScope) -> do
     vs <- forTeleWithPrefixM tele $ \h p s vs -> do
       let t = instantiateTele pure vs s
-      t' <- withVars vs $ elabExpr t -- TODO: This is a bit inefficient
+      t' <- withVars vs $ elabExpr mkConstraint t -- TODO: This is a bit inefficient
       forall h p t'
     let brExpr = instantiateTele pure vs brScope
-    brExpr' <- withVars vs $ elabExpr brExpr
+    brExpr' <- withVars vs $ elabExpr mkConstraint brExpr
     let abstr = teleAbstraction vs
     tele' <- Telescope
       <$> mapM (\v -> TeleArg (metaHint v) (metaData v) <$> abstractM abstr (metaType v)) vs
     brScope' <- abstractM abstr brExpr'
     return $ ConBranch qc tele' brScope'
   return $ ConBranches cbrs'
-elabBranches (LitBranches lbrs def) = LitBranches
-  <$> mapM (\(LitBranch l br) -> LitBranch l <$> elabExpr br) lbrs
-  <*> elabExpr def
+elabBranches mkConstraint (LitBranches lbrs def) = LitBranches
+  <$> mapM (\(LitBranch l br) -> LitBranch l <$> elabExpr mkConstraint br) lbrs
+  <*> elabExpr mkConstraint def
 
 elabDef
   :: Definition Expr MetaA
   -> AbstractM
   -> Infer (Definition Expr MetaA)
 elabDef (Definition i a e) _
-  = Definition i a <$> elabExpr e
+  = Definition i a <$> elabExpr mkConstraintVar e
 elabDef (DataDefinition (DataDef constrs) rep) typ = do
   typ' <- zonk typ
   let params = telescope typ'
@@ -202,10 +213,10 @@ elabDef (DataDefinition (DataDef constrs) rep) typ = do
   let abstr = teleAbstraction vs
   constrs' <- withVars vs $ forM constrs $ \constr -> forM constr $ \s -> do
     let e = instantiateTele pure vs s
-    e' <- elabExpr e
+    e' <- elabExpr mkConstraintVar e
     abstractM abstr e'
 
-  rep' <- elabExpr rep
+  rep' <- elabExpr mkConstraintVar rep
   return $ DataDefinition (DataDef constrs') rep'
 
 elabRecursiveDefs
@@ -214,10 +225,13 @@ elabRecursiveDefs
 elabRecursiveDefs defs
   = enterLevel
   $ forM defs $ \(v, def, typ) -> do
-    typ' <- elabExpr typ
+    typ' <- elabExpr mkConstraintVar typ
     def' <- elabDef def typ'
     return (v, def', typ')
 
+mkConstraintVar :: AbstractM -> Infer AbstractM
+mkConstraintVar = fmap pure . exists mempty Constraint
+
 mergeConstraintVars
   :: HashSet MetaA
   -> Infer ()
@@ -244,3 +258,19 @@ mergeConstraintVars = void . foldlM go mempty
             _ -> return $ Map.insert typ v varTypes
 
     go varTypes _ = return varTypes
+
+whnf :: AbstractM -> Infer AbstractM
+whnf = Normalise.whnf' Normalise.WhnfArgs
+  { Normalise.expandTypeReps = False
+  , Normalise.handleUnsolvedConstraint
+    = elabUnsolvedConstraint
+    $ return . Builtin.UnsolvedConstraint
+  }
+
+whnfExpandingTypeReps :: AbstractM -> Infer AbstractM
+whnfExpandingTypeReps = Normalise.whnf' Normalise.WhnfArgs
+  { Normalise.expandTypeReps = True
+  , Normalise.handleUnsolvedConstraint
+    = elabUnsolvedConstraint
+    $ return . Builtin.UnsolvedConstraint
+  }

src/Inference/Class.hs-boot

@@ -0,0 +1,6 @@
+module Inference.Class where
+
+import Inference.Monad
+import Meta
+
+whnf :: AbstractM -> Infer AbstractM

src/Inference/Monad.hs

@@ -1,12 +1,10 @@
-{-# LANGUAGE PatternSynonyms #-}
 module Inference.Monad where
 
 import Control.Monad.Reader
 
 import qualified Builtin.Names as Builtin
 import Meta
 import Syntax
-import Syntax.Abstract
 import VIX
 
 type Polytype = AbstractM
@@ -60,9 +58,6 @@ existsVar
   -> Plicitness
   -> AbstractM
   -> Infer AbstractM
-existsVar _ Constraint typ = return $ UnsolvedConstraint typ
+existsVar _ Constraint typ = return $ Builtin.UnsolvedConstraint typ
 existsVar h Implicit typ = pure <$> exists h Implicit typ
 existsVar h Explicit typ = pure <$> exists h Explicit typ
-
-pattern UnsolvedConstraint :: Expr v -> Expr v
-pattern UnsolvedConstraint typ = App (Global Builtin.UnsolvedConstraintName) Explicit typ